[isabelle-dev] [isabelle] match_tac, schematic and bound variables
makarius at sketis.net
Sat Aug 17 15:20:12 CEST 2013
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
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.)
More information about the isabelle-dev