On 17.08.2013 15:20, Makarius wrote:
On Thu, 15 Aug 2013, Lawrence Paulson wrote:
I think that the only way to achieve the documented behaviour is to
replace all schematic variables in the goal by Frees before attempting
resolution.
If you would do that for the quais-match mode of unify.ML in general it
would probably break down everything else.
Doing the above in user space instead, in the actual application at hand
(which was not explained on this thread so far) it might turn out trivial.
"Safe" application of rules in some sort of VCG (which is currently one
long Isar method expression).
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.
-- Lars
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
