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.
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. (Tools built on such high-level elements need
to be ready to work with renamings of the original schematic variables.
This is the normal situation in structured proof elements.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
