# HG changeset patch
# User blanchet
# Date 1354789510 -3600
# Node ID 78c7b52dbadbb61ac0ef6f7fc55d5ea58e7c81bb
# Parent  d84a5ab736bb23399cd3be049ce0c8961569b9c4
tweaked MaSh proximity

diff -r d84a5ab736bb -r 78c7b52dbadb src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Dec 06 11:25:10 2012 +0100
@@ -726,7 +726,7 @@
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =
-  Math.pow (1.3, 15.5 - 0.05 * Real.fromInt rank) + 15.0
+  Math.pow (1.3, 15.5 - 0.2 * Real.fromInt rank) + 15.0
 
 fun weight_proximity_facts facts =
   facts ~~ map weight_of_proximity_fact (0 upto length facts - 1)