equal
deleted
inserted
replaced
152 Node {context = context, facts = facts, mode = mode, goal = goal}; |
152 Node {context = context, facts = facts, mode = mode, goal = goal}; |
153 |
153 |
154 fun map_node f (Node {context, facts, mode, goal}) = |
154 fun map_node f (Node {context, facts, mode, goal}) = |
155 make_node (f (context, facts, mode, goal)); |
155 make_node (f (context, facts, mode, goal)); |
156 |
156 |
157 fun init ctxt = State (Stack.init (make_node (ctxt, NONE, Forward, NONE))); |
157 fun init ctxt = |
|
158 State (Stack.init (make_node (ProofContext.set_stmt true ctxt, NONE, Forward, NONE))); |
158 |
159 |
159 fun current (State st) = Stack.top st |> (fn Node node => node); |
160 fun current (State st) = Stack.top st |> (fn Node node => node); |
160 fun map_current f (State st) = State (Stack.map_top (map_node f) st); |
161 fun map_current f (State st) = State (Stack.map_top (map_node f) st); |
161 |
162 |
162 |
163 |