exported interface for explicit error messages

--- a/src/Pure/sorts.ML	Fri Jan 26 13:59:02 2007 +0100
+++ b/src/Pure/sorts.ML	Fri Jan 26 13:59:03 2007 +0100
@@ -47,6 +47,7 @@
   val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
     -> algebra -> (sort -> sort) * algebra
   type class_error
+  val msg_class_error: Pretty.pp -> class_error -> string
   val class_error: Pretty.pp -> class_error -> 'a
   exception CLASS_ERROR of class_error
   val mg_domain: algebra -> string -> sort -> sort list   (*exception CLASS_ERROR*)
@@ -306,10 +307,12 @@
 
 datatype class_error = NoClassrel of class * class | NoArity of string * class;
 
-fun class_error pp (NoClassrel (c1, c2)) =
-      error ("No class relation " ^ Pretty.string_of_classrel pp [c1, c2])
-  | class_error pp (NoArity (a, c)) =
-      error ("No type arity " ^ Pretty.string_of_arity pp (a, [], [c]));
+fun msg_class_error pp (NoClassrel (c1, c2)) =
+      "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
+  | msg_class_error pp (NoArity (a, c)) =
+      "No type arity " ^ Pretty.string_of_arity pp (a, [], [c]);
+
+fun class_error pp = error o msg_class_error pp;
 
 exception CLASS_ERROR of class_error;