On Wed, 10 Apr 2013, Johannes Hölzl wrote:
Unfortunately, as you mentioned the excpetion_trace output is not very
helpful, all I see is Seq.make / .copy / .append. The inner functions
which call Envir.var_clash is not shown.
It is relatively easy to instrument the main Seq.make abstraction itself.
Doing this, it points to Thm.bicompose_aux and Unify.unifiers, which is
the very core of "Isabelle" in the sense of the 1989 version.
I need to look more closely, and probably consult Stefan Berghofer as
well, who made the Envir.var_clash check many years ago -- before it was
just unchecked (and a comment written in Pure/ROOT.ML about something
important missing).
Stay tuned ...
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
