[isabelle-dev] [isabelle] match_tac, schematic and bound variables
lp15 at cam.ac.uk
Sat Aug 17 19:21:15 CEST 2013
Probably you are right.
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.)
More information about the isabelle-dev