equal
deleted
inserted
replaced
213 (pair I o Local_Theory.assert); |
213 (pair I o Local_Theory.assert); |
214 val ((_, _, _, lthy'), _) = lthy |
214 val ((_, _, _, lthy'), _) = lthy |
215 |> gen_includes get raw_incls |
215 |> gen_includes get raw_incls |
216 |> prep_decl ([], []) I raw_elems; |
216 |> prep_decl ([], []) I raw_elems; |
217 in |
217 in |
218 lthy' |> Local_Theory.init_target |
218 lthy' |> Local_Theory.begin_target after_close |
219 {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close} |
|
220 (Local_Theory.operations_of lthy) |
|
221 end; |
219 end; |
222 |
220 |
223 in |
221 in |
224 |
222 |
225 val unbundle = gen_activate Local_Theory.notes get_bundle; |
223 val unbundle = gen_activate Local_Theory.notes get_bundle; |