# 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