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. _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
