equal
deleted
inserted
replaced
142 |> Goal.norm_result |
142 |> Goal.norm_result |
143 |> PureThy.name_thm false false Position.none name; |
143 |> PureThy.name_thm false false Position.none name; |
144 |
144 |
145 in (result'', result) end; |
145 in (result'', result) end; |
146 |
146 |
147 fun note_local kind facts ctxt = |
|
148 ctxt |
|
149 |> ProofContext.qualified_names |
|
150 |> ProofContext.note_thmss_i kind facts |
|
151 ||> ProofContext.restore_naming ctxt; |
|
152 |
|
153 fun notes (Target {target, is_locale, ...}) kind facts lthy = |
147 fun notes (Target {target, is_locale, ...}) kind facts lthy = |
154 let |
148 let |
155 val thy = ProofContext.theory_of lthy; |
149 val thy = ProofContext.theory_of lthy; |
156 val facts' = facts |
150 val facts' = facts |
157 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
151 |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi |
163 |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |
157 |> is_locale ? Element.facts_map (Element.morph_ctxt (LocalTheory.target_morphism lthy)); |
164 val global_facts = PureThy.map_facts #2 facts' |
158 val global_facts = PureThy.map_facts #2 facts' |
165 |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy); |
159 |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy); |
166 in |
160 in |
167 lthy |> LocalTheory.theory |
161 lthy |> LocalTheory.theory |
168 (Sign.qualified_names |
162 (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd) |
169 #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd |
163 |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd) |
170 #> Sign.restore_naming thy) |
|
171 |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd) |
|
172 |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts) |
164 |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts) |
173 |> note_local kind local_facts |
165 |> ProofContext.note_thmss_i kind local_facts |
174 end; |
166 end; |
175 |
167 |
176 |
168 |
177 (* declare_const *) |
169 (* declare_const *) |
178 |
170 |