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.
tuned error message;
authorwenzelm
Tue, 31 Mar 2009 13:34:48 +0200
changeset 30815 e96498265a05
parent 30814 10dc9bc264b7
child 30816 4de62c902f9a
tuned error message;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 31 13:23:39 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 31 13:34:48 2009 +0200
@@ -582,8 +582,9 @@
       | (SOME S, NONE) => S
       | (SOME S, SOME S') =>
           if Type.eq_sort tsig (S, S') then S'
-          else error ("Sort constraint inconsistent with default for type variable " ^
-            quote (Term.string_of_vname' xi)));
+          else error ("Sort constraint " ^ Syntax.string_of_sort_global thy S ^
+            " inconsistent with default " ^ Syntax.string_of_sort_global thy S' ^
+            " for type variable " ^ quote (Term.string_of_vname' xi)));
   in get end;
 
 local
isabelle