[isabelle-dev] [isabelle] match_tac, schematic and bound variables

[Makarius]

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