src/Pure/Isar/locale.ML
changeset 46881 b81f1de9f57e
parent 46880 af8e516953ce
child 46893 d5bb4c212df1
equal deleted inserted replaced
46880:af8e516953ce 46881:b81f1de9f57e
   403     val mixin =
   403     val mixin =
   404       (case export' of
   404       (case export' of
   405         NONE => Morphism.identity
   405         NONE => Morphism.identity
   406       | SOME export => collect_mixins context (name, morph $> export) $> export);
   406       | SOME export => collect_mixins context (name, morph $> export) $> export);
   407     val morph' = transfer input $> morph $> mixin;
   407     val morph' = transfer input $> morph $> mixin;
   408     val notes' = map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
   408     val notes' =
       
   409       Par_List.map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
   409   in
   410   in
   410     fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
   411     fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
   411       notes' input
   412       notes' input
   412   end;
   413   end;
   413 
   414