# HG changeset patch
# User wenzelm
# Date 1331978108 -3600
# Node ID 23a59a495934f11558c284af9fad5103e3a0e193
# Parent  bd0ee92cabe741dd8c2fa87e3b2c78804871dbd8
tuned grouping -- merely indicate order of magnitude;

diff -r bd0ee92cabe7 -r 23a59a495934 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 17 10:54:15 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 17 10:55:08 2012 +0100
@@ -406,7 +406,7 @@
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
     val notes' =
-      grouped 50 Par_List.map
+      grouped 100 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)