# HG changeset patch
# User haftmann
# Date 1138605424 -3600
# Node ID 5fac129ae936e4cd5bb028b608502389f08b2687
# Parent  89b0fbbc4d8eb3f3427105e8a7e20435bfc56ec2
added map_atype, map_aterms

diff -r 89b0fbbc4d8e -r 5fac129ae936 src/Pure/term.ML
--- 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)