# HG changeset patch
# User wenzelm
# Date 1163105072 -3600
# Node ID 3340d0fcecd1e767de3a04f80b9ce46bf8283556
# Parent  3b01db9504a866b97ed3cefc903b040754625961
Stack.map_top;

diff -r 3b01db9504a8 -r 3340d0fcecd1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Nov 09 21:44:31 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Nov 09 21:44:32 2006 +0100
@@ -167,7 +167,7 @@
 fun init ctxt = State (Stack.init (make_node (ctxt, NONE, Forward, NONE)));
 
 fun current (State st) = Stack.top st |> (fn Node node => node);
-fun map_current f (State st) = State (Stack.map (map_node f) st);
+fun map_current f (State st) = State (Stack.map_top (map_node f) st);