tuned grouping -- merely indicate order of magnitude;

--- 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)