equal
deleted
inserted
replaced
218 local |
218 local |
219 |
219 |
220 fun gen_global_sublocale prep_loc prep_interpretation |
220 fun gen_global_sublocale prep_loc prep_interpretation |
221 raw_locale expression raw_defs raw_eqns thy = |
221 raw_locale expression raw_defs raw_eqns thy = |
222 let |
222 let |
223 val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy; |
223 val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
224 fun setup_proof after_qed = |
224 fun setup_proof after_qed = |
225 Element.witness_proof_eqs |
225 Element.witness_proof_eqs |
226 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
226 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
227 in |
227 in |
228 lthy |> |
228 lthy |> |