1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:07 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jun 26 13:35:12 2014 +0200
     1.3 @@ -441,7 +441,7 @@
     1.4      val _ = heap (Real.compare o pairself snd) num_facts num_facts overlaps_sqr
     1.5      val no_recommends = Unsynchronized.ref 0
     1.6      val recommends = Array.tabulate (num_facts, rpair 0.0)
     1.7 -    val age = Unsynchronized.ref 1000000000.0
     1.8 +    val age = Unsynchronized.ref 500000000.0
     1.9  
    1.10      fun inc_recommend j v =
    1.11        let val ov = snd (Array.sub (recommends, j)) in
    1.12 @@ -473,9 +473,14 @@
    1.13        handle EXIT () => ()
    1.14  
    1.15      fun ret acc at =
    1.16 -      if at = Array.length recommends then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
    1.17 +      if at = num_facts then acc else ret (Array.sub (recommends, at) :: acc) (at + 1)
    1.18    in
    1.19      while1 (); while2 ();
    1.20 +    List.app (fn at =>
    1.21 +        let val (j, ov) = Array.sub (recommends, at) in
    1.22 +          Array.update (recommends, at, (j, 1000000000.0 + ov))
    1.23 +        end)
    1.24 +      visible_facts;
    1.25      heap (Real.compare o pairself snd) max_suggs num_facts recommends;
    1.26      ret [] (Integer.max 0 (num_facts - max_suggs))
    1.27    end
    1.28 @@ -652,7 +657,7 @@
    1.29  
    1.30          val facts = rev rev_facts
    1.31          val fact_vec = Vector.fromList facts
    1.32 -        val int_visible_facts = map (Symtab.lookup fact_tab) visible_facts
    1.33 +        val int_visible_facts = map_filter (Symtab.lookup fact_tab) visible_facts
    1.34  
    1.35          val deps_vec = Vector.fromList (rev rev_depss)
    1.36