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