# HG changeset patch
# User wenzelm
# Date 1331978055 -3600
# Node ID bd0ee92cabe741dd8c2fa87e3b2c78804871dbd8
# Parent  80123a2202194dc7d260131cd765f04e35fe679d
slightly more parallel find_theorems;

diff -r 80123a220219 -r bd0ee92cabe7 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sat Mar 17 09:51:18 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Mar 17 10:54:15 2012 +0100
@@ -420,7 +420,10 @@
       then by the substitution size*)
     fun result_ord (((p0, s0), _), ((p1, s1), _)) =
       prod_ord int_ord int_ord ((p1, s1), (p0, s0));
-  in map_filter eval_filters theorems |> sort result_ord |> map #2 end;
+  in
+    grouped 100 Par_List.map eval_filters theorems
+    |> map_filter I |> sort result_ord |> map #2
+  end;
 
 fun lazy_filter filters =
   let
@@ -581,7 +584,7 @@
     (if null theorems then [Pretty.str "nothing found"]
      else
       [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
-        map (pretty_theorem ctxt) theorems)
+        grouped 10 Par_List.map (pretty_theorem ctxt) theorems)
   end |> Pretty.chunks |> Pretty.writeln;
 
 fun print_theorems ctxt =