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

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

     3.1 --- a/src/Pure/Isar/locale.ML	Mon Mar 12 23:16:54 2012 +0100
     3.2 +++ b/src/Pure/Isar/locale.ML	Mon Mar 12 23:33:50 2012 +0100
     3.3 @@ -406,7 +406,8 @@
     3.4        | SOME export => collect_mixins context (name, morph $> export) $> export);
     3.5      val morph' = transfer input $> morph $> mixin;
     3.6      val notes' =
     3.7 -      Par_List.map (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
     3.8 +      grouped 50 Par_List.map
     3.9 +        (Element.transform_ctxt morph' o Notes o #1) (#notes (the_locale thy name));
    3.10    in
    3.11      fold_rev (fn elem => fn res => activ_elem (Element.transform_ctxt (transfer res) elem) res)
    3.12        notes' input