(re)introduce (even more) aggressive parallelism, for the benefit of those users with dozens of CPU cores

--- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Dec 10 10:29:52 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Mon Dec 10 13:02:56 2012 +0100
@@ -17,6 +17,10 @@
 declare [[sledgehammer_instantiate_inducts]]
 
 ML {*
+! Multithreading.max_threads
+*}
+
+ML {*
 open MaSh_Eval
 *}
 

--- a/src/HOL/TPTP/mash_eval.ML	Mon Dec 10 10:29:52 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Mon Dec 10 13:02:56 2012 +0100
@@ -114,7 +114,7 @@
            fn () => prove mash_ok MaShN fst mash_facts,
            fn () => prove mesh_ok MeshN I mesh_facts,
            fn () => prove isar_ok IsarN fst isar_facts]
-          |> map (fn f => f ())
+          |> (* Par_List. *) map (fn f => f ())
       in
         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
          isar_s]
@@ -134,7 +134,7 @@
   in
     print " * * *";
     print ("Options: " ^ commas options);
-    List.app solve_goal (tag_list 1 lines);
+    Par_List.map solve_goal (tag_list 1 lines);
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,
      total_of MaShN mash_ok n,