Yes, it’s higher order unification behaving badly. There’s no simple way to control it; better to avoid the situation as I suggested. Larry Paulson On 24 Jan 2014, at 21:17, Manuel Eberl <eberlm at in.tum.de> wrote: > Could you please elaborate on what exactly is happening here? I've been > wondering about this myself for ages. Is it some kind of issue with > higher order unification?