# HG changeset patch
# User blanchet
# Date 1377512080 -7200
# Node ID 2a2dc18f3e10808fddc5e45bb2d4eb79cbf0ae8a
# Parent  09e8c42dbb061bc0e80a208299c081cfe230fab9
reverted 6c5e7143e1f6; took a better look at evaluation data this time

diff -r 09e8c42dbb06 -r 2a2dc18f3e10 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 26 11:42:35 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Aug 26 12:14:40 2013 +0200
@@ -904,7 +904,7 @@
 
 val chained_feature_factor = 0.5 (* FUDGE *)
 val extra_feature_factor = 0.1 (* FUDGE *)
-val num_extra_feature_facts = 5 (* FUDGE *)
+val num_extra_feature_facts = 10 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =