# HG changeset patch
# User blanchet
# Date 1381327653 -7200
# Node ID 4df62d7eae34276fc72036848c9d37f413ca653c
# Parent  a28992e35032d43c896b42e66fbe0b4683d99fc2
parallelize MeSh

diff -r a28992e35032 -r 4df62d7eae34 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Oct 09 15:58:02 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Oct 09 16:07:33 2013 +0200
@@ -1329,26 +1329,17 @@
                 (accepts |> filter_out in_add))
         |> take max_facts
       fun mepo () =
-        mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t
-                             facts
-        |> weight_facts_steeply
+        (mepo_suggested_facts ctxt params prover max_facts NONE hyp_ts concl_t facts
+         |> weight_facts_steeply, [])
       fun mash () =
-        mash_suggested_facts ctxt params prover (generous_max_facts max_facts)
-            hyp_ts concl_t facts
+        mash_suggested_facts ctxt params prover (generous_max_facts max_facts) hyp_ts concl_t facts
         |>> weight_facts_steeply
       val mess =
         (* the order is important for the "case" expression below *)
-        [] |> (if effective_fact_filter <> mepoN then
-                 cons (mash_weight, (mash ()))
-               else
-                 I)
-           |> (if effective_fact_filter <> mashN then
-                 cons (mepo_weight, (mepo (), []))
-               else
-                 I)
-      val mesh =
-        mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess
-        |> add_and_take
+        [] |> effective_fact_filter <> mepoN ? cons (mash_weight, mash)
+           |> effective_fact_filter <> mashN ? cons (mepo_weight, mepo)
+           |> Par_List.map (apsnd (fn f => f ()))
+      val mesh = mesh_facts (eq_snd Thm.eq_thm_prop) max_facts mess |> add_and_take
     in
       if save then MaSh.save ctxt overlord else ();
       case (fact_filter, mess) of