# HG changeset patch
# User blanchet
# Date 1377205403 -7200
# Node ID 5565d1b56f84f0663669c2e5a15b68e9b6305674
# Parent  c4e41658307a38675952f4dde839b0ed1c9e112d
increase relevance of unknown proximate facts

diff -r c4e41658307a -r 5565d1b56f84 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 23:03:22 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Aug 22 23:03:23 2013 +0200
@@ -927,18 +927,19 @@
 fun find_mash_suggestions _ _ [] _ _ raw_unknown = ([], raw_unknown)
   | find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
     let
+      val inter_fact = inter (Thm.eq_thm_prop o pairself snd)
       val raw_mash = find_suggested_facts ctxt facts suggs
-      val unknown_chained =
-        inter (Thm.eq_thm_prop o pairself snd) chained raw_unknown
-      val proximity = facts |> take max_proximity_facts
+      val proximate = take max_proximity_facts facts
+      val unknown_chained = inter_fact raw_unknown chained
+      val unknown_proximate = inter_fact raw_unknown proximate
       val mess =
-        [(0.90 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
-         (0.08 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown)),
-         (0.02 (* FUDGE *), (weight_facts_smoothly proximity, []))]
+        [(0.9 (* FUDGE *), (map (rpair 1.0) unknown_chained, [])),
+         (0.4 (* FUDGE *), (weight_facts_smoothly unknown_proximate, [])),
+         (0.1 (* FUDGE *), (weight_facts_steeply raw_mash, raw_unknown))]
       val unknown =
         raw_unknown
         |> fold (subtract (Thm.eq_thm_prop o pairself snd))
-                [unknown_chained, proximity]
+                [unknown_chained, unknown_proximate]
     in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end
 
 fun add_const_counts t =