some grouping of Par_List operations, to adjust granularity;

--- a/src/HOL/Tools/inductive.ML	Mon Mar 12 23:16:54 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Mar 12 23:33:50 2012 +0100
@@ -562,9 +562,9 @@
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val facts = args |> Par_List.map (fn ((a, atts), props) =>
+    val facts = args |> grouped 10 Par_List.map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
-        Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
   in lthy |> Local_Theory.notes facts |>> map snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop;

--- a/src/HOL/Tools/record.ML	Mon Mar 12 23:16:54 2012 +0100
+++ b/src/HOL/Tools/record.ML	Mon Mar 12 23:33:50 2012 +0100
@@ -2076,7 +2076,7 @@
 
     val (sel_convs, upd_convs) =
       timeit_msg ctxt "record sel_convs/upd_convs proof:" (fn () =>
-        Par_List.map (fn prop =>
+        grouped 10 Par_List.map (fn prop =>
           Skip_Proof.prove_global defs_thy [] [] prop
             (K (ALLGOALS (asm_full_simp_tac sel_upd_ss)))) (sel_conv_props @ upd_conv_props))
       |> chop (length sel_conv_props);

--- a/src/Pure/Isar/locale.ML	Mon Mar 12 23:16:54 2012 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Mar 12 23:33:50 2012 +0100
@@ -406,7 +406,8 @@
       | SOME export => collect_mixins context (name, morph $> export) $> export);
     val morph' = transfer input $> morph $> mixin;
     val notes' =
-      Par_List.map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
+      grouped 50 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)
       notes' input