inductive_cases: crude parallelization via Par_List.map;
authorwenzelm
Mon Jul 26 17:59:26 2010 +0200 (2010-07-26)
changeset 3795700e848690339
parent 37956 ee939247b2fb
child 37975 a79abb22ca9c
inductive_cases: crude parallelization via Par_List.map;
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Tools/inductive.ML	Mon Jul 26 17:41:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Mon Jul 26 17:59:26 2010 +0200
     1.3 @@ -522,9 +522,9 @@
     1.4  fun gen_inductive_cases prep_att prep_prop args lthy =
     1.5    let
     1.6      val thy = ProofContext.theory_of lthy;
     1.7 -    val facts = args |> map (fn ((a, atts), props) =>
     1.8 +    val facts = args |> Par_List.map (fn ((a, atts), props) =>
     1.9        ((a, map (prep_att thy) atts),
    1.10 -        map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
    1.11 +        Par_List.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;