equal
deleted
inserted
replaced
34 | switch_named_cmd (SOME name) (Context.Theory thy) = |
34 | switch_named_cmd (SOME name) (Context.Theory thy) = |
35 (end_named_cmd, context_begin_named_cmd [] name thy) |
35 (end_named_cmd, context_begin_named_cmd [] name thy) |
36 | switch_named_cmd NONE (Context.Proof lthy) = |
36 | switch_named_cmd NONE (Context.Proof lthy) = |
37 (Context.Proof o Local_Theory.reset, lthy) |
37 (Context.Proof o Local_Theory.reset, lthy) |
38 | switch_named_cmd (SOME name) (Context.Proof lthy) = |
38 | switch_named_cmd (SOME name) (Context.Proof lthy) = |
39 (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global, |
39 let |
40 (context_begin_named_cmd [] name o Local_Theory.exit_global_reinitializable) lthy); |
40 val (reinit, thy) = Named_Target.exit_global_reinitialize lthy |
|
41 in |
|
42 (Context.Proof o reinit o Local_Theory.exit_global, |
|
43 context_begin_named_cmd [] name thy) |
|
44 end; |
41 |
45 |
42 fun includes raw_includes lthy = |
46 fun includes raw_includes lthy = |
43 Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; |
47 Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; |
44 |
48 |
45 fun context_begin_nested_cmd raw_includes raw_elems gthy = |
49 fun context_begin_nested_cmd raw_includes raw_elems gthy = |