# HG changeset patch
# User blanchet
# Date 1354924130 -3600
# Node ID 5291606b21e23fb4b57f0897a47247a090616bd0
# Parent  e8f2d7a3ef5302297c95f9e92d4cc8044a94d529
use parallel map

diff -r e8f2d7a3ef53 -r 5291606b21e2 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sat Dec 08 00:48:50 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -42,7 +42,8 @@
     val isar_ok = Unsynchronized.ref 0
     fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
     fun index_string (j, s) = s ^ "@" ^ string_of_int j
-    fun str_of_res label facts ({outcome, run_time, used_facts, ...}: Sledgehammer_Provers.prover_result) =
+    fun str_of_res label facts ({outcome, run_time, used_facts, ...}
+                                : Sledgehammer_Provers.prover_result) =
       let val facts = facts |> map (fn ((name, _), _) => name ()) in
         "  " ^ label ^ ": " ^
         (if is_none outcome then
@@ -93,10 +94,12 @@
               run_prover_for_mash ctxt params prover facts goal
             val _ = if is_none outcome then ok := !ok + 1 else ()
           in str_of_res heading facts res end
-        val mepo_s = prove mepo_ok MePoN fst mepo_facts
-        val mash_s = prove mash_ok MaShN fst mash_facts
-        val mesh_s = prove mesh_ok MeshN I mesh_facts
-        val isar_s = prove isar_ok IsarN fst isar_facts
+        val [mepo_s, mash_s, mesh_s, isar_s] =
+          [fn () => prove mepo_ok MePoN fst mepo_facts,
+           fn () => prove mash_ok MaShN fst mash_facts,
+           fn () => prove mesh_ok MeshN I mesh_facts,
+           fn () => prove isar_ok IsarN fst isar_facts]
+          |> Par_List.map (fn f => f ())
       in
         ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s,
          isar_s]