# HG changeset patch
# User blanchet
# Date 1342817031 -7200
# Node ID 5493e67982ee1709b8a126ed271c8e9d290d29db
# Parent  47fe0ca12fc2c2a6ea0991bb62edf249f7748a4e
tune Mesh filter

diff -r 47fe0ca12fc2 -r 5493e67982ee src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:43:51 2012 +0200
@@ -613,7 +613,11 @@
     val suggs =
       if Graph.is_empty fact_G then []
       else mash_QUERY ctxt overlord (max_suggs_of max_facts) (parents, feats)
-    val selected = facts |> suggested_facts suggs
+    val selected =
+      facts |> suggested_facts suggs
+            (* The weights currently returned by "mash.py" are too extreme to
+               make any sense. *)
+            |> map fst |> weight_mepo_facts
     val unknown = facts |> filter_out (is_fact_in_graph fact_G)
   in (selected, unknown) end
 
@@ -653,7 +657,7 @@
           val feats = features_of ctxt prover thy (Local, General) [t]
           val deps = used_ths |> map nickname_of
           val {fact_G} = mash_get ctxt
-          val parents = timeit (fn () => maximal_in_graph fact_G facts)
+          val parents = maximal_in_graph fact_G facts
         in
           mash_ADD ctxt overlord [(name, parents, feats, deps)]; (true, "")
         end)
diff -r 47fe0ca12fc2 -r 5493e67982ee src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Fri Jul 20 22:43:51 2012 +0200
@@ -21,7 +21,7 @@
   val mepo_suggested_facts :
     Proof.context -> params -> string -> int -> relevance_fudge option
     -> term list -> term -> fact list -> fact list
-  val weight_mepo_facts : fact list -> (fact * real) list
+  val weight_mepo_facts : ('a * thm) list -> (('a * thm) * real) list
 end;
 
 structure Sledgehammer_MePo : SLEDGEHAMMER_MEPO =