[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Wed Apr 10 22:41:09 CEST 2013
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
Stay tuned ...
More information about the isabelle-dev