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

[Lars Noschinski]

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