removed unused material;

--- a/src/Pure/General/stack.ML	Sat Sep 01 19:43:18 2012 +0200
+++ b/src/Pure/General/stack.ML	Sat Sep 01 19:46:21 2012 +0200
@@ -10,9 +10,7 @@
   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*)
@@ -29,16 +27,8 @@
 
 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);

--- a/src/Pure/Isar/proof.ML	Sat Sep 01 19:43:18 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Sep 01 19:46:21 2012 +0200
@@ -169,10 +169,7 @@
   State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
 
 fun top (State st) = Stack.top st |> (fn Node node => node);
-fun bottom (State st) = Stack.bottom st |> (fn Node node => node);
-
 fun map_top f (State st) = State (Stack.map_top (map_node f) st);
-fun map_bottom f (State st) = State (Stack.map_bottom (map_node f) st);
 fun map_all f (State st) = State (Stack.map_all (map_node f) st);
 
 
@@ -210,9 +207,6 @@
 fun map_context_result f state =
   f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
 
-fun map_context_bottom f =
-  map_bottom (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
-
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
 fun propagate_ml_env state = map_contexts