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

[Lawrence Paulson]

Probably you are right.
Larry

On 17 Aug 2013, at 14:20, Makarius <makarius at sketis.net> 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.
> 
> 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