# HG changeset patch
# User nipkow
# Date 754571417 -3600
# Node ID 58d54dc482d17e124b2b04369ec420eee4bdc5b3
# Parent  d77bd6c76c03259b55d50e9a01f39abadb90c02c
added logical_types

diff -r d77bd6c76c03 -r 58d54dc482d1 src/Pure/type.ML
--- 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