[isabelle-dev] auto raises a TYPE exception

[Makarius]

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