Stack.map_top;
authorwenzelm
Thu, 09 Nov 2006 21:44:32 +0100
changeset 21274 3340d0fcecd1
parent 21273 3b01db9504a8
child 21275 e4cb9c7a7482
Stack.map_top;
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);