# HG changeset patch
# User wenzelm
# Date 1163105070 -3600
# Node ID a87b27cdd142efd1c716d67afd547acb067518ed
# Parent  4f791faf33f41391e8dcf768f5126bbab809bcdb
separate map_top/all;

diff -r 4f791faf33f4 -r a87b27cdd142 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Thu Nov 09 21:44:29 2006 +0100
+++ b/src/Pure/General/stack.ML	Thu Nov 09 21:44:30 2006 +0100
@@ -11,7 +11,8 @@
   val level: 'a T -> int
   val init: 'a -> 'a T
   val top: 'a T -> 'a
-  val map: ('a -> 'a) -> 'a T -> 'a T
+  val map_top: ('a -> 'a) -> 'a T -> 'a T
+  val map_all: ('a -> 'a) -> 'a T -> 'a T
   val push: 'a T -> 'a T
   val pop: 'a T -> 'a T      (*exception Empty*)
 end;
@@ -27,7 +28,9 @@
 
 fun top (x, _) = x;
 
-fun map f (x, xs) = (f x, xs);
+fun map_top f (x, xs) = (f x, xs);
+
+fun map_all f (x, xs) = (f x, map f xs);
 
 fun push (x, xs) = (x, x :: xs);