--- a/src/Pure/type.ML Tue May 04 12:30:15 2010 +0200
+++ b/src/Pure/type.ML Tue May 04 14:38:59 2010 +0200
@@ -53,6 +53,7 @@
val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
(*special treatment of type vars*)
+ val sort_of_atyp: typ -> sort
val strip_sorts: typ -> typ
val no_tvars: typ -> typ
val varify_global: (string * sort) list -> term -> ((string * sort) * indexname) list * term
@@ -271,6 +272,13 @@
(** special treatment of type vars **)
+(* sort_of_atyp *)
+
+fun sort_of_atyp (TFree (_, S)) = S
+ | sort_of_atyp (TVar (_, S)) = S
+ | sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
+
+
(* strip_sorts *)
fun strip_sorts (Type (a, Ts)) = Type (a, map strip_sorts Ts)