# HG changeset patch # User blanchet # Date 1354924131 -3600 # Node ID 330d4ad89e92e99accac9ebd865063323e3bbefd # Parent 9bb7868a4c200d02e71e7de1a35bf99ee166aada reverted parallel map idea -- appears to make success rate of ATPs less stable (might even lead to bias in favor of MePo) diff -r 9bb7868a4c20 -r 330d4ad89e92 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:51 2012 +0100 @@ -103,7 +103,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] - |> Par_List.map (fn f => f ()) + |> map (fn f => f ()) in ["Goal " ^ string_of_int j ^ ": " ^ name, mepo_s, mash_s, mesh_s, isar_s]