163 val thy = ProofContext.theory_of lthy; |
163 val thy = ProofContext.theory_of lthy; |
164 val facts' = facts |
164 val facts' = facts |
165 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
165 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
166 (Local_Theory.full_name lthy (fst a))) bs)) |
166 (Local_Theory.full_name lthy (fst a))) bs)) |
167 |> PureThy.map_facts (import_export_proof lthy); |
167 |> PureThy.map_facts (import_export_proof lthy); |
168 val local_facts = PureThy.map_facts #1 facts' |
168 val local_facts = PureThy.map_facts #1 facts'; |
169 |> Attrib.map_facts (Attrib.attribute_i thy); |
|
170 val target_facts = PureThy.map_facts #1 facts' |
|
171 |> is_locale ? Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)); |
|
172 val global_facts = PureThy.map_facts #2 facts' |
169 val global_facts = PureThy.map_facts #2 facts' |
173 |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy); |
170 |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy); |
174 in |
171 in |
175 lthy |
172 lthy |
176 |> Local_Theory.theory (PureThy.note_thmss kind global_facts #> snd) |
173 |> Local_Theory.theory (PureThy.note_thmss kind global_facts #> snd) |
177 |> not is_locale ? Local_Theory.target (ProofContext.note_thmss kind global_facts #> snd) |
174 |> not is_locale ? Local_Theory.target (ProofContext.note_thmss kind global_facts #> snd) |
178 |> is_locale ? Local_Theory.target (Locale.add_thmss target kind target_facts) |
175 |> is_locale ? Local_Theory.target (Locale.add_thmss target kind |
179 |> ProofContext.note_thmss kind local_facts |
176 (Element.facts_map (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts)) |
|
177 |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts) |
180 end; |
178 end; |
181 |
179 |
182 |
180 |
183 (* mixfix notation *) |
181 (* mixfix notation *) |
184 |
182 |