src/Pure/sorts.ML

   val empty_algebra: algebra
   val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
   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*)
   val of_sort: algebra -> typ * sort -> bool
   val of_sort_derivation: Pretty.pp -> algebra ->

 
 (* errors *)
 
 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;
 
 
 (* mg_domain *)