[isabelle-dev] [isabelle] Higher-order matching against schematic variables

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 19 13:28:21 CET 2010

Looking at this again, I'm not certain there is a bug. You are displaying the variable assignments, but are you first applying the type variable assignments? Both must be used in order to instantiate the object term.

On 19 Nov 2010, at 11:11, Michael Chan wrote:

> I can confirm that the first lemma's matcher 4. and the second lemma's only matcher are results of the FO matcher. So, I guess the above question becomes: how come the FO matcher doesn't instantiate the type variables? Of course, this is a different question to why the HO matcher doesn't return matchers to the second lemma.

More information about the isabelle-dev mailing list