separate map_top/all;

--- 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);