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