eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
--- 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)