Probably you are right. Larry On 17 Aug 2013, at 14:20, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
