# HG changeset patch
# User wenzelm
# Date 1437854049 -7200
# Node ID c4d3da84d8841fbc2e01e0cb9b1dbbbb0254e398
# Parent  682c0dd89b268c70a5a69a3d0b0691ae5eb6817e
clarified error;

diff -r 682c0dd89b26 -r c4d3da84d884 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Sat Jul 25 21:37:09 2015 +0200
+++ b/src/Pure/drule.ML	Sat Jul 25 21:54:09 2015 +0200
@@ -769,14 +769,13 @@
                   val t = Var (xi, T);
                   val u = Thm.term_of cu;
                 in
-                  raise TYPE ("Ill-typed instantiation:\nType\n" ^
-                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^
-                    "\nof variable " ^
+                  raise THM ("infer_instantiate: type " ^
+                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^
                     Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
-                    "\ncannot be unified with type\n" ^
-                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^
+                    "\ncannot be unified with type " ^
+                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ " of term " ^
                     Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
-                    [T, U], [t, u])
+                    0, [th])
                 end;
           in (((xi, T), cu), (tyenv', maxidx')) end;