equal
deleted
inserted
replaced
423 val mixin = |
423 val mixin = |
424 (case export' of |
424 (case export' of |
425 NONE => Morphism.identity |
425 NONE => Morphism.identity |
426 | SOME export => collect_mixins context (name, morph $> export) $> export); |
426 | SOME export => collect_mixins context (name, morph $> export) $> export); |
427 val facts' = facts |
427 val facts' = facts |
428 |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin)); |
428 |> Element.facts_map (Element.transform_ctxt (transfer input $> morph $> mixin)); |
429 in activ_elem (Notes (kind, facts')) input end; |
429 in activ_elem (Notes (kind, facts')) input end; |
430 in |
430 in |
431 fold_rev activate notes input |
431 fold_rev activate notes input |
432 end; |
432 end; |
433 |
433 |
560 ((change_locale loc o apfst o apsnd) (cons (args', serial ())) |
560 ((change_locale loc o apfst o apsnd) (cons (args', serial ())) |
561 #> |
561 #> |
562 (* Registrations *) |
562 (* Registrations *) |
563 (fn thy => fold_rev (fn (_, morph) => |
563 (fn thy => fold_rev (fn (_, morph) => |
564 let |
564 let |
565 val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |> |
565 val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |> |
566 Attrib.map_facts (Attrib.attribute_i thy) |
566 Attrib.map_facts (Attrib.attribute_i thy) |
567 in Global_Theory.note_thmss kind args'' #> snd end) |
567 in Global_Theory.note_thmss kind args'' #> snd end) |
568 (registrations_of (Context.Theory thy) loc) thy)) |
568 (registrations_of (Context.Theory thy) loc) thy)) |
569 in ctxt'' end; |
569 in ctxt'' end; |
570 |
570 |