equal
deleted
inserted
replaced
161 ||> ProofContext.restore_naming ctxt; |
161 ||> ProofContext.restore_naming ctxt; |
162 |
162 |
163 fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy = |
163 fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy = |
164 let |
164 let |
165 val thy = ProofContext.theory_of lthy; |
165 val thy = ProofContext.theory_of lthy; |
166 val full = LocalTheory.full_name lthy; |
|
167 |
|
168 val facts' = facts |
166 val facts' = facts |
169 |> map (fn (a, bs) => |
167 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
170 (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs)) |
168 (LocalTheory.full_name lthy (fst a))) bs)) |
171 |> PureThy.map_facts (import_export_proof lthy); |
169 |> PureThy.map_facts (import_export_proof lthy); |
172 val local_facts = PureThy.map_facts #1 facts' |
170 val local_facts = PureThy.map_facts #1 facts' |
173 |> Attrib.map_facts (Attrib.attribute_i thy); |
171 |> Attrib.map_facts (Attrib.attribute_i thy); |
174 val target_facts = PureThy.map_facts #1 facts' |
172 val target_facts = PureThy.map_facts #1 facts' |
175 |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |
173 |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |