# HG changeset patch
# User wenzelm
# Date 863521354 -7200
# Node ID 02d32516bc92453ade9465ea80e30d06063cdc24
# Parent  aceb79945d683d1c9ef240e1a9d1fc4cfe216d26
of_sort: type_sig -> typ * sort -> bool;

diff -r aceb79945d68 -r 02d32516bc92 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] [];