# HG changeset patch
# User haftmann
# Date 1211817335 -7200
# Node ID 197af793312c145e8bf5c34932b4a7970695f897
# Parent  b952df8d505b5ba88047793c5cd293b0533d3ef5
proper NoSubsort CLASS_ERROR

diff -r b952df8d505b -r 197af793312c src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon May 26 17:55:34 2008 +0200
+++ b/src/Pure/sorts.ML	Mon May 26 17:55:35 2008 +0200
@@ -314,8 +314,9 @@
       "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
   | class_error pp (NoArity (a, c)) =
       "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
-  | class_error pp (NoSubsort (s1, s2)) =
-      Pretty.string_of_sort pp s1 ^ " is not a subsort of " ^ Pretty.string_of_sort pp s2;
+  | class_error pp (NoSubsort (S1, S2)) =
+     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
+       ^ " < " ^ Pretty.string_of_sort pp S2;
 
 exception CLASS_ERROR of class_error;
 
@@ -383,8 +384,7 @@
     fun weakens S1 S2 = S2 |> map (fn c2 =>
       (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
         SOME d1 => weaken d1 c2
-      | NONE => error ("Cannot derive subsort relation " ^
-          Pretty.string_of_sort pp (map #2 S1) ^ " < " ^ Pretty.string_of_sort pp S2)));
+      | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
 
     fun derive _ [] = []
       | derive (Type (a, Ts)) S =