equal
deleted
inserted
replaced
163 fun map_node f (Node {context, facts, mode, goal}) = |
163 fun map_node f (Node {context, facts, mode, goal}) = |
164 make_node (f (context, facts, mode, goal)); |
164 make_node (f (context, facts, mode, goal)); |
165 |
165 |
166 val init_context = |
166 val init_context = |
167 Proof_Context.set_stmt true #> |
167 Proof_Context.set_stmt true #> |
168 Proof_Context.map_naming (K Proof_Context.local_naming); |
168 Proof_Context.map_naming (K Name_Space.local_naming); |
169 |
169 |
170 fun init ctxt = |
170 fun init ctxt = |
171 State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); |
171 State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); |
172 |
172 |
173 fun current (State st) = Stack.top st |> (fn Node node => node); |
173 fun current (State st) = Stack.top st |> (fn Node node => node); |