slightly more parallel find_theorems;
authorwenzelm
Sat, 17 Mar 2012 10:54:15 +0100
changeset 46977 bd0ee92cabe7
parent 46976 80123a220219
child 46978 23a59a495934
slightly more parallel find_theorems;
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 =