--- a/src/Pure/type.ML Mon Nov 29 12:00:57 1993 +0100
+++ b/src/Pure/type.ML Mon Nov 29 12:10:17 1993 +0100
@@ -21,6 +21,7 @@
-> term * (indexname*typ)list
val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term
val logical_type: type_sig -> string -> bool
+ val logical_types: type_sig -> string list
val merge: type_sig * type_sig -> type_sig
val thaw_vars: typ -> typ
val tsig0: type_sig
@@ -119,6 +120,9 @@
| None => undcl_type_err(t)
end;
+fun logical_types (tsig as TySg {args, ...}) =
+ filter (logical_type tsig) (map #1 args);
+
(* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1