# HG changeset patch
# User wenzelm
# Date 880558637 -3600
# Node ID a09e3e6da2de26b67dc5aa894c2451d003877a76
# Parent  05af145a61d4c3a07a38fd2f21e8ca455e409c39
added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
added foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a;
added foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a;

diff -r 05af145a61d4 -r a09e3e6da2de src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Nov 26 16:35:39 1997 +0100
+++ b/src/Pure/term.ML	Wed Nov 26 16:37:17 1997 +0100
@@ -699,6 +699,26 @@
 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
 
 
+(* left-ro-right traversal *)
+
+(*foldl atoms of type*)
+fun foldl_atyps f (x, Type (_, Ts)) = foldl (foldl_atyps f) (x, Ts)
+  | foldl_atyps f x_atom = f x_atom;
+
+(*foldl atoms of term*)
+fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
+  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
+  | foldl_aterms f x_atom = f x_atom;
+
+(*foldl types of term*)
+fun foldl_types f (x, Const (_, T)) = f (x, T)
+  | foldl_types f (x, Free (_, T)) = f (x, T)
+  | foldl_types f (x, Var (_, T)) = f (x, T)
+  | foldl_types f (x, Bound _) = x
+  | foldl_types f (x, Abs (_, T, t)) = foldl_types f (f (x, T), t)
+  | foldl_types f (x, t $ u) = foldl_types f (foldl_types f (x, t), u);
+
+
 
 (*** Compression of terms and types by sharing common subtrees.  
      Saves 50-75% on storage requirements.  As it is fairly slow,