# HG changeset patch
# User wenzelm
# Date 861357471 -7200
# Node ID 271062b8c461d43b3cb1604eef5351c8d2d115cd
# Parent  8189a4870d196f6a2cfb988e1af681fed2731c6e
removed least_sort;
added of_sort;

diff -r 8189a4870d19 -r 271062b8c461 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Apr 18 11:55:14 1997 +0200
+++ b/src/Pure/sorts.ML	Fri Apr 18 11:57:51 1997 +0200
@@ -21,7 +21,7 @@
   val inter_class: classrel -> class * sort -> sort
   val inter_sort: classrel -> sort * sort -> sort
   val norm_sort: classrel -> sort -> sort
-  val least_sort: classrel -> arities -> typ -> sort
+  val of_sort: classrel -> arities -> typ * sort -> bool
   val mg_domain: classrel -> arities -> string -> sort -> sort list
   val nonempty_sort: classrel -> arities -> sort list -> sort -> bool
 end;
@@ -134,22 +134,6 @@
 
 (** sorts of types **)
 
-(* least_sort *)
-
-fun least_sort classrel arities T =
-  let
-    fun match_dom Ss (c, Ss') =
-      if sorts_le classrel (Ss, Ss') then Some c
-      else None;
-
-    fun leastS (Type (a, Ts)) =
-          norm_sort classrel
-            (mapfilter (match_dom (map leastS Ts)) (assocs arities a))
-      | leastS (TFree (_, S)) = S
-      | leastS (TVar (_, S)) = S
-  in leastS T end;
-
-
 (* mg_domain *)                 (*exception TYPE*)
 
 fun mg_dom arities a c =
@@ -164,6 +148,20 @@
       end;
 
 
+(* of_sort *)
+
+fun of_sort classrel arities =
+  let
+    fun ofS (_, []) = true
+      | ofS (TFree (_, S), S') = sort_le classrel (S, S')
+      | ofS (TVar (_, S), S') = sort_le classrel (S, S')
+      | ofS (Type (a, Ts), S) =
+          let val Ss = mg_domain classrel arities a S in
+            ListPair.all ofS (Ts, Ss)
+          end handle TYPE _ => false;
+  in ofS end;
+
+
 
 (** nonempty_sort **)