# HG changeset patch
# User berghofe
# Date 1196174611 -3600
# Node ID ba5a2bb7a81ad3bb05b1650eb919e1332e2804ff
# Parent  f81b3be9dfdd1d4498a146bfa3e10f8137c2f9db
Better error messages for cterm_instantiate.

diff -r f81b3be9dfdd -r ba5a2bb7a81a src/Pure/drule.ML
--- 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