# HG changeset patch
# User wenzelm
# Date 1519140577 -3600
# Node ID 175a070e9dd86fb4cf88de5b6eb3fde9c16037b5
# Parent  8fd84fe1d60bf3e1a2a62b49aaa4529c1c6fc686
eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);

diff -r 8fd84fe1d60b -r 175a070e9dd8 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Feb 20 16:20:36 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Feb 20 16:29:37 2018 +0100
@@ -457,7 +457,7 @@
         NONE => Morphism.identity
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
-    val notes' = grouped 100 Par_List.map (Element.transform_ctxt morph') (lazy_notes thy name);
+    val notes' = map (Element.transform_ctxt morph') (lazy_notes thy name);
   in
     (notes', input) |-> fold (fn elem => fn res =>
       activ_elem (Element.transform_ctxt (transfer res) elem) res)