--- a/src/Pure/drule.ML Mon Nov 26 22:59:24 2007 +0100
+++ b/src/Pure/drule.ML Tue Nov 27 15:43:31 2007 +0100
@@ -830,7 +830,14 @@
val maxi = Int.max(maxidx, Int.max(maxt, maxu));
val thy' = Theory.merge(thy, Theory.merge(thyt, thyu))
val (tye',maxi') = Sign.typ_unify thy' (T, U) (tye, maxi)
- handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
+ handle Type.TUNIFY => raise TYPE ("Ill-typed instantiation:\nType\n" ^
+ Sign.string_of_typ thy' (Envir.norm_type tye T) ^
+ "\nof variable " ^
+ Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) t) ^
+ "\ncannot be unified with type\n" ^
+ Sign.string_of_typ thy' (Envir.norm_type tye U) ^ "\nof term " ^
+ Sign.string_of_term thy' (Term.map_types (Envir.norm_type tye) u),
+ [T, U], [t, u])
in (thy', tye', maxi') end;
in
fun cterm_instantiate [] th = th