1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:38:15 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:56:28 2014 +0200
     1.3 @@ -404,8 +404,8 @@
     1.4  
     1.5      val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
     1.6  
     1.7 -    fun inc_overlap j v =
     1.8 -      let val ov = snd (Array.sub (overlaps_sqr, j)) in
     1.9 +    fun inc_overlap v j =
    1.10 +      let val (_, ov) = Array.sub (overlaps_sqr, j) in
    1.11          Array.update (overlaps_sqr, j, (j, v + ov))
    1.12        end
    1.13  
    1.14 @@ -413,9 +413,8 @@
    1.15        let
    1.16          val sw = sw0 * tfidf s
    1.17          val w2 = sw * sw
    1.18 -        fun do_th j = if j < num_facts then inc_overlap j w2 else ()
    1.19        in
    1.20 -        List.app do_th (Array.sub (feat_facts, s))
    1.21 +        List.app (inc_overlap w2) (Array.sub (feat_facts, s))
    1.22        end
    1.23  
    1.24      val _ = List.app do_feat goal_feats