1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 11:56:28 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 27 12:06:22 2014 +0200
     1.3 @@ -404,17 +404,17 @@
     1.4  
     1.5      val overlaps_sqr = Array.tabulate (num_facts, rpair 0.0)
     1.6  
     1.7 -    fun inc_overlap v j =
     1.8 -      let val (_, ov) = Array.sub (overlaps_sqr, j) in
     1.9 -        Array.update (overlaps_sqr, j, (j, v + ov))
    1.10 -      end
    1.11 -
    1.12      fun do_feat (s, sw0) =
    1.13        let
    1.14          val sw = sw0 * tfidf s
    1.15          val w2 = sw * sw
    1.16 +
    1.17 +        fun inc_overlap j =
    1.18 +          let val (_, ov) = Array.sub (overlaps_sqr, j) in
    1.19 +            Array.update (overlaps_sqr, j, (j, w2 + ov))
    1.20 +          end
    1.21        in
    1.22 -        List.app (inc_overlap w2) (Array.sub (feat_facts, s))
    1.23 +        List.app inc_overlap (Array.sub (feat_facts, s))
    1.24        end
    1.25  
    1.26      val _ = List.app do_feat goal_feats
    1.27 @@ -424,7 +424,7 @@
    1.28      val age = Unsynchronized.ref 500000000.0
    1.29  
    1.30      fun inc_recommend j v =
    1.31 -      let val ov = snd (Array.sub (recommends, j)) in
    1.32 +      let val (_, ov) = Array.sub (recommends, j) in
    1.33          if ov <= 0.0 then
    1.34            (no_recommends := !no_recommends + 1; Array.update (recommends, j, (j, !age + ov)))
    1.35          else if ov < !age + 1000.0 then
    1.36 @@ -1275,7 +1275,7 @@
    1.37  
    1.38  val chained_feature_factor = 0.5 (* FUDGE *)
    1.39  val extra_feature_factor = 0.05 (* FUDGE *)
    1.40 -val num_extra_feature_facts = 10 (* FUDGE *)
    1.41 +val num_extra_feature_facts = 0 (* FUDGE *)
    1.42  
    1.43  (* FUDGE *)
    1.44  fun weight_of_proximity_fact rank =