# HG changeset patch
# User wenzelm
# Date 1208097608 -7200
# Node ID 454d11701fa453517a1c9ada67d0784e36010a6e
# Parent  cf67665296c2f6062bb407bd522ec054036282b3
Sorts.class_error: produce message only (formerly msg_class_error);

diff -r cf67665296c2 -r 454d11701fa4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 13 16:40:07 2008 +0200
+++ b/src/Pure/Isar/class.ML	Sun Apr 13 16:40:08 2008 +0200
@@ -707,7 +707,7 @@
               (Consts.typargs consts c_ty) sorts)
       | matchings _ = I
     val tvartab = (fold o fold_aterms) matchings ts Vartab.empty
-      handle Sorts.CLASS_ERROR e => Sorts.class_error pp e;
+      handle Sorts.CLASS_ERROR e => error (Sorts.class_error pp e);
     val inst = map_type_tvar (fn (vi, _) => TVar (vi, the (Vartab.lookup tvartab vi)));
   in if Vartab.is_empty tvartab then NONE else SOME ((map o map_types) inst ts) end;
 
diff -r cf67665296c2 -r 454d11701fa4 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Sun Apr 13 16:40:07 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML	Sun Apr 13 16:40:08 2008 +0200
@@ -115,7 +115,7 @@
             val tys = Sign.const_typargs thy (c, ty);
             val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
           in fn tab => fold2 (curry (Sorts.meet_sort algebra)) tys sorts tab
-            handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.msg_class_error pp e ^ ",\n"
+            handle Sorts.CLASS_ERROR e => raise CLASS_ERROR ([c], Sorts.class_error pp e ^ ",\n"
               ^ "for constant " ^ CodeUnit.string_of_const thy c
               ^ "\nin defining equations(s)\n"
               ^ (cat_lines o map string_of_thm) thms)