slightly more parallel find_theorems;
authorwenzelm
Sat, 17 Mar 2012 10:54:15 +0100
changeset 47851bd0ee92cabe7
parent 47850 80123a220219
child 47852 23a59a495934
slightly more parallel find_theorems;
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Mar 17 09:51:18 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Mar 17 10:54:15 2012 +0100
     1.3 @@ -420,7 +420,10 @@
     1.4        then by the substitution size*)
     1.5      fun result_ord (((p0, s0), _), ((p1, s1), _)) =
     1.6        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
     1.7 -  in map_filter eval_filters theorems |> sort result_ord |> map #2 end;
     1.8 +  in
     1.9 +    grouped 100 Par_List.map eval_filters theorems
    1.10 +    |> map_filter I |> sort result_ord |> map #2
    1.11 +  end;
    1.12  
    1.13  fun lazy_filter filters =
    1.14    let
    1.15 @@ -581,7 +584,7 @@
    1.16      (if null theorems then [Pretty.str "nothing found"]
    1.17       else
    1.18        [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
    1.19 -        map (pretty_theorem ctxt) theorems)
    1.20 +        grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
    1.21    end |> Pretty.chunks |> Pretty.writeln;
    1.22  
    1.23  fun print_theorems ctxt =