eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
authorwenzelm
Tue, 20 Feb 2018 16:29:37 +0100
changeset 67680 175a070e9dd8
parent 67679 8fd84fe1d60b
child 67681 b5058ba95e32
eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
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)