# HG changeset patch
# User blanchet
# Date 1377500852 -7200
# Node ID 6c5e7143e1f65695a807a687a57a345e24969091
# Parent  942a1b48bb310ce4637d9b920e4099fe350ba4be
tuned fudge factor in light of evaluation

diff -r 942a1b48bb31 -r 6c5e7143e1f6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 25 23:20:25 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 26 09:07:32 2013 +0200
@@ -902,9 +902,9 @@
 
 fun is_fact_in_graph access_G = can (Graph.get_node access_G) o nickname_of_thm
 
-val chained_feature_factor = 0.5
-val extra_feature_factor = 0.1
-val num_extra_feature_facts = 10 (* FUDGE *)
+val chained_feature_factor = 0.5 (* FUDGE *)
+val extra_feature_factor = 0.1 (* FUDGE *)
+val num_extra_feature_facts = 5 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =