[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Stefan Berghofer wrote:

>  Types as well as terms are unified.  The outermost functions assume
>  the terms to be unified already have the same type.  In resolution,
>  this is assured because both have type "prop".

One more aspect here: HO unification is also used on flex-flex pairs, 
which might have different types.  The unify implementation might 
correctly produce equal types for other reasons nonetheless, but the 
"proof" above would have to be adapted.

Note that the marginal change 6228806b2605 in metis_reconstruct.ML is 
related to that: without applying the type instantiation on the matched 
flex-flex pairs it could break down.


 	Makarius