Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
activate_notes in parallel -- to speedup main operation of locale interpretation;
authorwenzelm
Mon, 12 Mar 2012 21:31:22 +0100
changeset 46881 b81f1de9f57e
parent 46880 af8e516953ce
child 46890 38171cab67ae
activate_notes in parallel -- to speedup main operation of locale interpretation;
src/Pure/Isar/locale.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle