added logical_types
authornipkow
Mon Nov 29 12:10:17 1993 +0100 (1993-11-29)
changeset 16258d54dc482d1
parent 161 d77bd6c76c03
child 163 ad90d96c2ec3
added logical_types
src/Pure/type.ML
     1.1 --- a/src/Pure/type.ML	Mon Nov 29 12:00:57 1993 +0100
     1.2 +++ b/src/Pure/type.ML	Mon Nov 29 12:10:17 1993 +0100
     1.3 @@ -21,6 +21,7 @@
     1.4  		   -> term * (indexname*typ)list
     1.5    val inst_term_tvars: type_sig * (indexname * typ)list -> term -> term
     1.6    val logical_type: type_sig -> string -> bool
     1.7 +   val logical_types: type_sig -> string list
     1.8    val merge: type_sig * type_sig -> type_sig
     1.9    val thaw_vars: typ -> typ
    1.10    val tsig0: type_sig
    1.11 @@ -119,6 +120,9 @@
    1.12      | None => undcl_type_err(t)
    1.13    end;
    1.14  
    1.15 +fun logical_types (tsig as TySg {args, ...}) =
    1.16 +  filter (logical_type tsig) (map #1 args);
    1.17 +
    1.18  
    1.19  (* 'sortorder' checks the ordering on sets of classes,i.e. on sorts:
    1.20     S1 <= S2 ,iff for every class C2 in S2 there exists a class C1 in S1