diff -r 72808e956879 -r 9c68e43502ce src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Thu Aug 30 16:39:50 2012 +0200
+++ b/src/Pure/General/stack.ML	Thu Aug 30 19:18:49 2012 +0200
@@ -10,7 +10,9 @@
   val level: 'a T -> int
   val init: 'a -> 'a T
   val top: 'a T -> 'a
+  val bottom: 'a T -> 'a
   val map_top: ('a -> 'a) -> 'a T -> 'a T
+  val map_bottom: ('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 List.Empty*)
@@ -27,8 +29,16 @@
 
 fun top (x, _) = x;
 
+fun bottom (x, []) = x
+  | bottom (_, xs) = List.last xs;
+
 fun map_top f (x, xs) = (f x, xs);
 
+fun map_bottom f (x, []) = (f x, [])
+  | map_bottom f (x, rest) =
+      let val (ys, z) = split_last rest
+      in (x, ys @ [f z]) end;
+
 fun map_all f (x, xs) = (f x, map f xs);
 
 fun push (x, xs) = (x, x :: xs);