# HG changeset patch
# User wenzelm
# Date 1280159966 -7200
# Node ID 00e848690339ceb039eeb8b3f9ccb4af021f2aa8
# Parent  ee939247b2fb180c9c0f4693cf925b6f7ebf94b1
inductive_cases: crude parallelization via Par_List.map;

diff -r ee939247b2fb -r 00e848690339 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon Jul 26 17:41:26 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon Jul 26 17:59:26 2010 +0200
@@ -522,9 +522,9 @@
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val facts = args |> map (fn ((a, atts), props) =>
+    val facts = args |> Par_List.map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
-        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
+        Par_List.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;