equal
deleted
inserted
replaced
112 |
112 |
113 (* local theory wrappers *) |
113 (* local theory wrappers *) |
114 |
114 |
115 type generic_theory = Context.generic; (*theory or local_theory*) |
115 type generic_theory = Context.generic; (*theory or local_theory*) |
116 |
116 |
117 val loc_init = TheoryTarget.init; |
117 val loc_init = TheoryTarget.init_cmd; |
118 |
118 |
119 val loc_exit = ProofContext.theory_of o LocalTheory.exit; |
119 val loc_exit = ProofContext.theory_of o LocalTheory.exit; |
120 |
120 |
121 fun loc_begin loc (Context.Theory thy) = loc_init loc thy |
121 fun loc_begin loc (Context.Theory thy) = loc_init loc thy |
122 | loc_begin NONE (Context.Proof lthy) = lthy |
122 | loc_begin NONE (Context.Proof lthy) = lthy |