# 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]