equal
deleted
inserted
replaced
156 |> Goal.norm_result |
156 |> Goal.norm_result |
157 |> PureThy.name_thm false false name; |
157 |> PureThy.name_thm false false name; |
158 |
158 |
159 in (result'', result) end; |
159 in (result'', result) end; |
160 |
160 |
161 fun theory_notes kind global_facts local_facts lthy = |
161 fun theory_notes kind global_facts lthy = |
162 let |
162 let |
163 val thy = ProofContext.theory_of lthy; |
163 val thy = ProofContext.theory_of lthy; |
164 val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; |
164 val global_facts' = Attrib.map_facts (Attrib.attribute_i thy) global_facts; |
165 in |
165 in |
166 lthy |
166 lthy |
188 val local_facts = PureThy.map_facts #1 facts'; |
188 val local_facts = PureThy.map_facts #1 facts'; |
189 val global_facts = PureThy.map_facts #2 facts'; |
189 val global_facts = PureThy.map_facts #2 facts'; |
190 in |
190 in |
191 lthy |
191 lthy |
192 |> (if is_locale then locale_notes target kind global_facts local_facts |
192 |> (if is_locale then locale_notes target kind global_facts local_facts |
193 else theory_notes kind global_facts local_facts) |
193 else theory_notes kind global_facts) |
194 |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts) |
194 |> ProofContext.note_thmss kind (Attrib.map_facts (Attrib.attribute_i thy) local_facts) |
195 end; |
195 end; |
196 |
196 |
197 |
197 |
198 (* consts in locales *) |
198 (* consts in locales *) |
249 end; |
249 end; |
250 |
250 |
251 |
251 |
252 (* abbrev *) |
252 (* abbrev *) |
253 |
253 |
|
254 fun theory_abbrev prmode ((b, mx), t) = Local_Theory.theory |
|
255 (Sign.add_abbrev (#1 prmode) (b, t) #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx)])); |
|
256 |
|
257 fun locale_abbrev ta prmode ((b, mx), t) xs = Local_Theory.theory_result |
|
258 (Sign.add_abbrev Print_Mode.internal (b, t)) #-> (fn (lhs, _) => |
|
259 syntax_declaration ta false (locale_const ta prmode ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)))); |
|
260 |
254 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy = |
261 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy = |
255 let |
262 let |
256 val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy); |
263 val thy_ctxt = ProofContext.init_global (ProofContext.theory_of lthy); |
257 val target_ctxt = Local_Theory.target_of lthy; |
264 val target_ctxt = Local_Theory.target_of lthy; |
258 |
265 |
266 |
273 |
267 val global_rhs = |
274 val global_rhs = |
268 singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; |
275 singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u; |
269 in |
276 in |
270 lthy |> |
277 lthy |> |
271 (if is_locale then |
278 (if is_locale then locale_abbrev ta prmode ((b, mx2), global_rhs) xs #> |
272 Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) |
279 is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) |
273 #-> (fn (lhs, _) => |
280 else theory_abbrev prmode ((b, mx3), global_rhs)) |
274 let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in |
|
275 syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #> |
|
276 is_class ? class_target ta (Class_Target.abbrev target prmode ((b, mx1), t')) |
|
277 end) |
|
278 else |
|
279 Local_Theory.theory |
|
280 (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => |
|
281 Sign.notation true prmode [(lhs, mx3)]))) |
|
282 |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd |
281 |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd |
283 |> Local_Defs.fixed_abbrev ((b, NoSyn), t) |
282 |> Local_Defs.fixed_abbrev ((b, NoSyn), t) |
284 end; |
283 end; |
285 |
284 |
286 |
285 |