# HG changeset patch
# User blanchet
# Date 1422882093 -3600
# Node ID 90f5bab83c3184f2792796a340a10399aa62c13c
# Parent  8300c4ddf4938f94d7e103b876d2b2397a86160c
tuning

diff -r 8300c4ddf493 -r 90f5bab83c31 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 30 17:29:51 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Feb 02 14:01:33 2015 +0100
@@ -350,7 +350,7 @@
         val (res, sfh) = fold add_feat goal_feats (init_val * Math.ln tfreq, Vector.sub (sfreq, i))
 
         fun fold_sfh (f, sf) sow =
-          sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq)
+          sow + tfidf f * Math.ln (1.0 - Real.fromInt (sf - 1) / tfreq)
 
         val sum_of_weights = Inttab.fold fold_sfh sfh 0.0
       in
@@ -385,7 +385,7 @@
     fun do_feat (s, sw0) =
       let
         val sw = sw0 * tfidf s
-        val w6 = Math.pow (sw, 6.0)
+        val w6 = Math.pow (sw, 6.0 (* FUDGE *))
 
         fun inc_overlap j =
           let val (_, ov) = Array.sub (overlaps_sqr, j) in
@@ -405,7 +405,8 @@
       let val (_, ov) = Array.sub (recommends, j) in
         if ov <= 0.0 then
           (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
-        else Array.update (recommends, j, (j, v + ov))
+        else
+          Array.update (recommends, j, (j, v + ov))
       end
 
     val k = Unsynchronized.ref 0