proper NoSubsort CLASS_ERROR
authorhaftmann
Mon May 26 17:55:35 2008 +0200 (2008-05-26)
changeset 26994197af793312c
parent 26993 b952df8d505b
child 26995 2511a72dd73c
proper NoSubsort CLASS_ERROR
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Mon May 26 17:55:34 2008 +0200
     1.2 +++ b/src/Pure/sorts.ML	Mon May 26 17:55:35 2008 +0200
     1.3 @@ -314,8 +314,9 @@
     1.4        "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
     1.5    | class_error pp (NoArity (a, c)) =
     1.6        "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
     1.7 -  | class_error pp (NoSubsort (s1, s2)) =
     1.8 -      Pretty.string_of_sort pp s1 ^ " is not a subsort of " ^ Pretty.string_of_sort pp s2;
     1.9 +  | class_error pp (NoSubsort (S1, S2)) =
    1.10 +     "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
    1.11 +       ^ " < " ^ Pretty.string_of_sort pp S2;
    1.12  
    1.13  exception CLASS_ERROR of class_error;
    1.14  
    1.15 @@ -383,8 +384,7 @@
    1.16      fun weakens S1 S2 = S2 |> map (fn c2 =>
    1.17        (case S1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
    1.18          SOME d1 => weaken d1 c2
    1.19 -      | NONE => error ("Cannot derive subsort relation " ^
    1.20 -          Pretty.string_of_sort pp (map #2 S1) ^ " < " ^ Pretty.string_of_sort pp S2)));
    1.21 +      | NONE => raise CLASS_ERROR (NoSubsort (map #2 S1, S2))));
    1.22  
    1.23      fun derive _ [] = []
    1.24        | derive (Type (a, Ts)) S =