On Sun, 18 Aug 2013, Lars Noschinski wrote:
Combinators like Subgoal.FOCUS have replaced a lot of old-style
tinkering with goals; within the focused parts things are fixed and
don't get instantiated by accident.
I seem to remember a discussion on the mailing list that Subgoal.FOCUS
does not export schematic type variables. So this would give us another
not-quite correct match implementation.
I still have this on my list to look after it in further detail, but as
far as I can tell it was about situations that are conceptially not
allowed anyway: schematic type variables within fixed-term variables.
The inference kernel happens to allow that in primitive rules, but almost
everything will break down. Type-inference is part of the syntactic
phase, and needs to be finished before doing the actual logical
inferencing.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
