modernized datatype constructors;
authorwenzelm
Sun Apr 11 14:06:35 2010 +0200 (2010-04-11)
changeset 3610542c37cf849cd
parent 36104 fecb587a1d0e
child 36106 19deea200358
modernized datatype constructors;
src/Pure/sorts.ML
     1.1 --- a/src/Pure/sorts.ML	Sun Apr 11 14:04:10 2010 +0200
     1.2 +++ b/src/Pure/sorts.ML	Sun Apr 11 14:06:35 2010 +0200
     1.3 @@ -335,15 +335,15 @@
     1.4  (* errors -- performance tuning via delayed message composition *)
     1.5  
     1.6  datatype class_error =
     1.7 -  NoClassrel of class * class |
     1.8 -  NoArity of string * class |
     1.9 -  NoSubsort of sort * sort;
    1.10 +  No_Classrel of class * class |
    1.11 +  No_Arity of string * class |
    1.12 +  No_Subsort of sort * sort;
    1.13  
    1.14 -fun class_error pp (NoClassrel (c1, c2)) =
    1.15 +fun class_error pp (No_Classrel (c1, c2)) =
    1.16        "No class relation " ^ Pretty.string_of_classrel pp [c1, c2]
    1.17 -  | class_error pp (NoArity (a, c)) =
    1.18 +  | class_error pp (No_Arity (a, c)) =
    1.19        "No type arity " ^ Pretty.string_of_arity pp (a, [], [c])
    1.20 -  | class_error pp (NoSubsort (S1, S2)) =
    1.21 +  | class_error pp (No_Subsort (S1, S2)) =
    1.22       "Cannot derive subsort relation " ^ Pretty.string_of_sort pp S1
    1.23         ^ " < " ^ Pretty.string_of_sort pp S2;
    1.24  
    1.25 @@ -357,7 +357,7 @@
    1.26      val arities = arities_of algebra;
    1.27      fun dom c =
    1.28        (case AList.lookup (op =) (Symtab.lookup_list arities a) c of
    1.29 -        NONE => raise CLASS_ERROR (NoArity (a, c))
    1.30 +        NONE => raise CLASS_ERROR (No_Arity (a, c))
    1.31        | SOME (_, Ss) => Ss);
    1.32      fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
    1.33    in
    1.34 @@ -375,7 +375,7 @@
    1.35      fun meet _ [] = I
    1.36        | meet (TFree (_, S)) S' =
    1.37            if sort_le algebra (S, S') then I
    1.38 -          else raise CLASS_ERROR (NoSubsort (S, S'))
    1.39 +          else raise CLASS_ERROR (No_Subsort (S, S'))
    1.40        | meet (TVar (v, S)) S' =
    1.41            if sort_le algebra (S, S') then I
    1.42            else Vartab.map_default (v, S) (inters S')
    1.43 @@ -417,7 +417,7 @@
    1.44            S2 |> map (fn c2 =>
    1.45              (case D1 |> find_first (fn (_, c1) => class_le algebra (c1, c2)) of
    1.46                SOME d1 => class_relation T d1 c2
    1.47 -            | NONE => raise CLASS_ERROR (NoSubsort (S1, S2))))
    1.48 +            | NONE => raise CLASS_ERROR (No_Subsort (S1, S2))))
    1.49        end;
    1.50  
    1.51      fun derive (_, []) = []
    1.52 @@ -442,7 +442,7 @@
    1.53    in
    1.54      fn (x, c1) => fn c2 =>
    1.55        (case Graph.irreducible_paths (classes_of algebra) (c1, c2) of
    1.56 -        [] => raise CLASS_ERROR (NoClassrel (c1, c2))
    1.57 +        [] => raise CLASS_ERROR (No_Classrel (c1, c2))
    1.58        | cs :: _ => path (x, cs))
    1.59    end;
    1.60