[isabelle-dev] auto raises a TYPE exception

[Christian Sternagel]

> Hopefully it is all a bit more precise now.  Maybe someone wants to
> formalize pattern.ML + unify.ML after > 20 years, to pin down the
> remaining uncertaincies about type instantiation within these
> non-trivial algorithms.
Just for the record, I would be interested in joining such an endeavor. 
Unfortunately I'm not a proven expert ;)

cheers

chris