# HG changeset patch # User wenzelm # Date 1331584282 -3600 # Node ID b81f1de9f57e326cff698286e4752f331eaa6f4c # Parent af8e516953cebc308181629c093f655b9a7affbb activate_notes in parallel -- to speedup main operation of locale interpretation; diff -r af8e516953ce -r b81f1de9f57e src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Mon Mar 12 20:44:10 2012 +0100 +++ b/src/Pure/Isar/locale.ML Mon Mar 12 21:31:22 2012 +0100 @@ -405,7 +405,8 @@ NONE => Morphism.identity | SOME export => collect_mixins context (name, morph $> export) $> export); val morph' = transfer input $> morph $> mixin; - val notes' = map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name)); + val notes' = + Par_List.map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name)); in fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res) notes' input