--- a/src/Pure/term.ML Sun Jan 29 19:24:56 2006 +0100
+++ b/src/Pure/term.ML Mon Jan 30 08:17:04 2006 +0100
@@ -64,6 +64,8 @@
val strip_comb: term -> term * term list
val head_of: term -> term
val size_of_term: term -> int
+ val map_atyps: (typ -> typ) -> typ -> typ
+ val map_aterms: (term -> term) -> term -> term
val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
val map_type_tfree: (string * sort -> typ) -> typ -> typ
val map_term_types: (typ -> typ) -> term -> term
@@ -435,6 +437,13 @@
| add_size (_, n) = n + 1;
in add_size (tm, 0) end;
+fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
+ | map_atyps f T = T;
+
+fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
+ | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
+ | map_aterms f t = f t;
+
fun map_type_tvar f =
let
fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)