Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified error;
authorwenzelm
Sat, 25 Jul 2015 21:54:09 +0200
changeset 60779 c4d3da84d884
parent 60778 682c0dd89b26
child 60780 7e2c8a63a8f8
clarified error;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle