# HG changeset patch # User wenzelm # Date 925488136 -7200 # Node ID 9b108dd75c2515ebda719b077b3c1603440950cd # Parent 5ba27aade76f9432e91c2603e58cbb1a2d78b7d8 val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term; diff -r 5ba27aade76f -r 9b108dd75c25 src/Pure/term.ML --- a/src/Pure/term.ML Fri Apr 30 18:01:55 1999 +0200 +++ b/src/Pure/term.ML Fri Apr 30 18:02:16 1999 +0200 @@ -67,6 +67,7 @@ val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a + val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term val dummyT: typ val logicC: class val logicS: sort @@ -892,6 +893,13 @@ | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t) | foldl_aterms f x_atom = f x_atom; +fun foldl_map_aterms f (x, t $ u) = + let val (x', t') = foldl_map_aterms f (x, t); val (x'', u') = foldl_map_aterms f (x', u); + in (x'', t' $ u') end + | foldl_map_aterms f (x, Abs (a, T, t)) = + let val (x', t') = foldl_map_aterms f (x, t) in (x', Abs (a, T, t')) end + | foldl_map_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)