# HG changeset patch
# User blanchet
# Date 1354924130 -3600
# Node ID e8f2d7a3ef5302297c95f9e92d4cc8044a94d529
# Parent  960a3429615c21e640573f75ee5209c0cc11c2fb
tweak MaSh fudge factors

diff -r 960a3429615c -r e8f2d7a3ef53 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 08 00:48:50 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -465,8 +465,8 @@
     end
 
 fun thy_feature_of s = ("y" ^ s, 0.5 (* FUDGE *))
-fun const_feature_of s = ("c" ^ s, 1.0 (* FUDGE *))
-fun free_feature_of s = ("f" ^ s, 2.0 (* FUDGE *))
+fun const_feature_of s = ("c" ^ s, 4.0 (* FUDGE *))
+fun free_feature_of s = ("f" ^ s, 5.0 (* FUDGE *))
 fun type_feature_of s = ("t" ^ s, 0.5 (* FUDGE *))
 fun class_feature_of s = ("s" ^ s, 0.25 (* FUDGE *))
 fun status_feature_of status = (string_of_status status, 0.5 (* FUDGE *))
@@ -722,9 +722,6 @@
 fun is_fact_in_graph fact_G (_, th) =
   can (Graph.get_node fact_G) (nickname_of th)
 
-(* factor that controls whether unknown global facts should be included *)
-val include_unk_global_factor = 15
-
 (* use MePo weights for now *)
 val weight_raw_mash_facts = weight_mepo_facts
 val weight_mash_facts = weight_raw_mash_facts
@@ -745,9 +742,9 @@
             |> map fst
     val proximity = facts |> sort (thm_ord o pairself snd o swap)
     val mess =
-      [(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, []))]
+      [(0.80 (* FUDGE *), (map (rpair 1.0) chained, [])),
+       (0.16 (* FUDGE *), (weight_raw_mash_facts raw_mash, unknown)),
+       (0.04 (* FUDGE *), (weight_proximity_facts proximity, []))]
   in mesh_facts max_facts mess end
 
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts