src/Pure/Isar/locale.ML
changeset 67680 175a070e9dd8
parent 67677 ac4b475fc8c3
child 67694 ab68ca1e80ba
equal deleted inserted replaced
67679:8fd84fe1d60b 67680:175a070e9dd8
   455     val mixin =
   455     val mixin =
   456       (case export' of
   456       (case export' of
   457         NONE => Morphism.identity
   457         NONE => Morphism.identity
   458       | SOME export => collect_mixins context (name, morph $> export) $> export);
   458       | SOME export => collect_mixins context (name, morph $> export) $> export);
   459     val morph' = transfer input $> morph $> mixin;
   459     val morph' = transfer input $> morph $> mixin;
   460     val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
   460     val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name);
   461   in
   461   in
   462     (notes', input) |-> fold (fn elem => fn res =>
   462     (notes', input) |-> fold (fn elem => fn res =>
   463       activ_elem (Element.transform_ctxt (transfer res) elem) res)
   463       activ_elem (Element.transform_ctxt (transfer res) elem) res)
   464   end handle ERROR msg => activate_err msg (name, morph) context;
   464   end handle ERROR msg => activate_err msg (name, morph) context;
   465 
   465