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 =