equal
deleted
inserted
replaced
189 local |
189 local |
190 |
190 |
191 fun gen_global_sublocale prep_loc prep_interpretation |
191 fun gen_global_sublocale prep_loc prep_interpretation |
192 raw_locale expression raw_defs thy = |
192 raw_locale expression raw_defs thy = |
193 let |
193 let |
194 val lthy = Named_Target.init (prep_loc thy raw_locale) thy; |
194 val lthy = Named_Target.init [] (prep_loc thy raw_locale) thy; |
195 fun setup_proof after_qed = |
195 fun setup_proof after_qed = |
196 Element.witness_proof_eqs |
196 Element.witness_proof_eqs |
197 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
197 (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit); |
198 in |
198 in |
199 lthy |> |
199 lthy |> |