# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID c69a970143c0889b28436cdeaf015227c618e1df
# Parent  835a18063ed59612fd89684c2de21fa80731a6e4
prioritize chained facts

diff -r 835a18063ed5 -r c69a970143c0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -754,13 +754,12 @@
             (* The weights currently returned by "mash.py" are too spaced out to
                make any sense. *)
             |> map fst
-    val proximity =
-      chained @ (facts |> subtract (Thm.eq_thm_prop o pairself snd) chained
-                       |> sort (thm_ord o pairself snd o swap))
+    val proximity = facts |> sort (thm_ord o pairself snd o swap)
     val unknown = facts |> filter_out (is_fact_in_graph fact_G)
     val mess =
-      [(0.667 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
-       (0.333 (* FUDGE *), (weight_proximity_facts proximity, []))]
+      [(0.8000 (* FUDGE *), (map (rpair 1.0) chained, [])),
+       (0.1333 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
+       (0.0667 (* FUDGE *), (weight_proximity_facts proximity, []))]
   in mesh_facts max_facts mess end
 
 fun add_wrt_fact_graph ctxt (name, parents, feats, deps) (adds, graph) =