# HG changeset patch
# User blanchet
# Date 1403862988 -7200
# Node ID b532b879acd06c28b6dae36143e82021e447e62d
# Parent  02f56126b4e41dad7bcd8a3e6fe0ef0763036b70
tuning

diff -r 02f56126b4e4 -r b532b879acd0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:38:15 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:56:28 2014 +0200
@@ -404,8 +404,8 @@
 
     val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
 
-    fun inc_overlap j v =
-      let val ov = snd (Array.sub (overlaps_sqr, j)) in
+    fun inc_overlap v j =
+      let val (_, ov) = Array.sub (overlaps_sqr, j) in
         Array.update (overlaps_sqr, j, (j, v + ov))
       end
 
@@ -413,9 +413,8 @@
       let
         val sw = sw0 * tfidf s
         val w2 = sw * sw
-        fun do_th j = if j < num_facts then inc_overlap j w2 else ()
       in
-        List.app do_th (Array.sub (feat_facts, s))
+        List.app (inc_overlap w2) (Array.sub (feat_facts, s))
       end
 
     val _ = List.app do_feat goal_feats