of_sort: type_sig -> typ * sort -> bool;
authorwenzelm
Tue, 13 May 1997 13:02:34 +0200
changeset 3175 02d32516bc92
parent 3174 aceb79945d68
child 3176 a3db6c177885
of_sort: type_sig -> typ * sort -> bool;
src/Pure/type.ML
--- a/src/Pure/type.ML	Mon May 12 18:44:43 1997 +0200
+++ b/src/Pure/type.ML	Tue May 13 13:02:34 1997 +0200
@@ -54,6 +54,7 @@
   val typ_match: type_sig -> (indexname * typ) list * (typ * typ)
     -> (indexname * typ) list
   val typ_instance: type_sig * typ * typ -> bool
+  val of_sort: type_sig -> typ * sort -> bool
 
   (*type unification*)
   exception TUNIFY
@@ -268,8 +269,11 @@
   in map_type_tvar inst end;
 
 
-fun check_has_sort (TySg {classrel, arities, ...}, T, S) =
-  if Sorts.of_sort classrel arities (T, S) then ()
+
+fun of_sort (TySg {classrel, arities, ...}) = Sorts.of_sort classrel arities;
+
+fun check_has_sort (tsig, T, S) =
+  if of_sort tsig (T, S) then ()
   else raise_type ("Type not of sort " ^ Sorts.str_of_sort S) [T] [];