--- a/src/Pure/sorts.ML Mon Jun 21 16:39:58 2004 +0200
+++ b/src/Pure/sorts.ML Mon Jun 21 16:40:08 2004 +0200
@@ -26,6 +26,8 @@
val inter_class: classes -> class * sort -> sort
val inter_sort: classes -> sort * sort -> sort
val norm_sort: classes -> sort -> sort
+ val certify_class: classes -> class -> class
+ val certify_sort: classes -> sort -> sort
val of_sort: classes * arities -> typ * sort -> bool
exception DOMAIN of string * class
val mg_domain: classes * arities -> string -> sort -> sort list (*exception DOMAIN*)
@@ -119,11 +121,30 @@
(* normal forms of sorts *)
+local
+
fun minimal_class classes S c =
not (exists (fn c' => class_less classes (c', c)) S);
-fun norm_sort classes S =
- sort_strings (distinct (filter (minimal_class classes S) S));
+val distinct_class = gen_distinct (op = : class * class -> bool);
+
+in
+
+fun norm_sort _ [] = []
+ | norm_sort _ (S as [_]) = S
+ | norm_sort classes S =
+ sort_strings (distinct_class (filter (minimal_class classes S) S));
+
+end;
+
+
+(* certify *)
+
+fun certify_class classes c =
+ if can (Graph.get_node classes) c then c
+ else raise TYPE ("Undeclared class: " ^ quote c, [], []);
+
+fun certify_sort classes = norm_sort classes o map (certify_class classes);