--- 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 =