added map_atype, map_aterms
authorhaftmann
Mon Jan 30 08:17:04 2006 +0100 (2006-01-30)
changeset 188475fac129ae936
parent 18846 89b0fbbc4d8e
child 18848 4ed69fe8f887
added map_atype, map_aterms
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Sun Jan 29 19:24:56 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Mon Jan 30 08:17:04 2006 +0100
     1.3 @@ -64,6 +64,8 @@
     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 map_atyps: (typ -> typ) -> typ -> typ
     1.8 +  val map_aterms: (term -> term) -> term -> term
     1.9    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
    1.10    val map_type_tfree: (string * sort -> typ) -> typ -> typ
    1.11    val map_term_types: (typ -> typ) -> term -> term
    1.12 @@ -435,6 +437,13 @@
    1.13        | add_size (_, n) = n + 1;
    1.14    in add_size (tm, 0) end;
    1.15  
    1.16 +fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
    1.17 +  | map_atyps f T = T;
    1.18 +
    1.19 +fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
    1.20 +  | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
    1.21 +  | map_aterms f t = f t;
    1.22 +
    1.23  fun map_type_tvar f =
    1.24    let
    1.25      fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)