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

[Lawrence Paulson]

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.
Larry

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.