# HG changeset patch
# User blanchet
# Date 1403863582 -7200
# Node ID 5e65e3d108a168df99c6d0562f6477a86976963a
# Parent  b532b879acd06c28b6dae36143e82021e447e62d
tuning

diff -r b532b879acd0 -r 5e65e3d108a1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:56:28 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 12:06:22 2014 +0200
@@ -404,17 +404,17 @@
 
     val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
 
-    fun inc_overlap v j =
-      let val (_, ov) = Array.sub (overlaps_sqr, j) in
-        Array.update (overlaps_sqr, j, (j, v + ov))
-      end
-
     fun do_feat (s, sw0) =
       let
         val sw = sw0 * tfidf s
         val w2 = sw * sw
+
+        fun inc_overlap j =
+          let val (_, ov) = Array.sub (overlaps_sqr, j) in
+            Array.update (overlaps_sqr, j, (j, w2 + ov))
+          end
       in
-        List.app (inc_overlap w2) (Array.sub (feat_facts, s))
+        List.app inc_overlap (Array.sub (feat_facts, s))
       end
 
     val _ = List.app do_feat goal_feats
@@ -424,7 +424,7 @@
     val age = Unsynchronized.ref 500000000.0
 
     fun inc_recommend j v =
-      let val ov = snd (Array.sub (recommends, j)) in
+      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 if ov < !age + 1000.0 then
@@ -1275,7 +1275,7 @@
 
 val chained_feature_factor = 0.5 (* FUDGE *)
 val extra_feature_factor = 0.05 (* FUDGE *)
-val num_extra_feature_facts = 10 (* FUDGE *)
+val num_extra_feature_facts = 0 (* FUDGE *)
 
 (* FUDGE *)
 fun weight_of_proximity_fact rank =