src/Pure/term.ML
changeset 29882 29154e67731d
parent 29286 5de880bda02d
child 30144 56ae4893e8ae
child 30240 5b25fee0362c
     1.1 --- a/src/Pure/term.ML	Thu Feb 12 12:35:45 2009 -0800
     1.2 +++ b/src/Pure/term.ML	Fri Feb 13 07:53:38 2009 +1100
     1.3 @@ -64,6 +64,7 @@
     1.4    val strip_comb: term -> term * term list
     1.5    val head_of: term -> term
     1.6    val size_of_term: term -> int
     1.7 +  val size_of_typ: typ -> int
     1.8    val map_atyps: (typ -> typ) -> typ -> typ
     1.9    val map_aterms: (term -> term) -> term -> term
    1.10    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    1.11 @@ -391,6 +392,13 @@
    1.12        | add_size (_, n) = n + 1;
    1.13    in add_size (tm, 0) end;
    1.14  
    1.15 +(*number of tfrees, tvars, and constructors in a type*)
    1.16 +fun size_of_typ ty =
    1.17 +  let
    1.18 +    fun add_size (Type (_, ars), n) = foldl add_size (n + 1) ars
    1.19 +      | add_size (_, n) = n + 1;
    1.20 +  in add_size (ty, 0) end;
    1.21 +
    1.22  fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
    1.23    | map_atyps f T = f T;
    1.24