# HG changeset patch
# User wenzelm
# Date 1238499288 -7200
# Node ID e96498265a05f1a79dd0927f238f53332ca25aae
# Parent  10dc9bc264b7f6af23da57aab047d02a9be37846
tuned error message;

diff -r 10dc9bc264b7 -r e96498265a05 src/Pure/Isar/proof_context.ML
--- 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