--- a/src/Pure/term.ML Thu Feb 12 12:35:45 2009 -0800
+++ b/src/Pure/term.ML Fri Feb 13 07:53:38 2009 +1100
@@ -64,6 +64,7 @@
val strip_comb: term -> term * term list
val head_of: term -> term
val size_of_term: term -> int
+ val size_of_typ: typ -> int
val map_atyps: (typ -> typ) -> typ -> typ
val map_aterms: (term -> term) -> term -> term
val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
@@ -391,6 +392,13 @@
| add_size (_, n) = n + 1;
in add_size (tm, 0) end;
+(*number of tfrees, tvars, and constructors in a type*)
+fun size_of_typ ty =
+ let
+ fun add_size (Type (_, ars), n) = foldl add_size (n + 1) ars
+ | add_size (_, n) = n + 1;
+ in add_size (ty, 0) end;
+
fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
| map_atyps f T = f T;