1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 24 18:46:38 2014 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4  fun weight_facts_smoothly facts = facts ~~ map smooth_weight_of_fact (0 upto length facts - 1)
     1.5  fun weight_facts_steeply facts = facts ~~ map steep_weight_of_fact (0 upto length facts - 1)
     1.6  
     1.7 -fun rev_sort_array_prefix cmp bnd a =
     1.8 +fun sort_array_suffix cmp needed a =
     1.9    let
    1.10      exception BOTTOM of int
    1.11  
    1.12 @@ -246,7 +246,7 @@
    1.13      fun for i = if i < 0 then () else (trickle al i (Array.sub (a, i)); for (i - 1))
    1.14  
    1.15      fun for2 i =
    1.16 -      if i < Integer.max 2 (al - bnd) then
    1.17 +      if i < Integer.max 2 (al - needed) then
    1.18          ()
    1.19        else
    1.20          let val e = Array.sub (a, i) in
    1.21 @@ -266,10 +266,10 @@
    1.22        ()
    1.23    end
    1.24  
    1.25 -fun rev_sort_list_prefix cmp bnd xs =
    1.26 +fun rev_sort_list_prefix cmp needed xs =
    1.27    let val ary = Array.fromList xs in
    1.28 -    rev_sort_array_prefix cmp bnd ary;
    1.29 -    Array.foldr (op ::) [] ary
    1.30 +    sort_array_suffix cmp needed ary;
    1.31 +    Array.foldl (op ::) [] ary
    1.32    end
    1.33  
    1.34  
    1.35 @@ -363,7 +363,7 @@
    1.36        if at = num_facts then acc else ret (at + 1) (Array.sub (posterior, at) :: acc)
    1.37    in
    1.38      select_visible_facts 100000.0 posterior visible_facts;
    1.39 -    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs posterior;
    1.40 +    sort_array_suffix (Real.compare o pairself snd) max_suggs posterior;
    1.41      ret (Integer.max 0 (num_facts - max_suggs)) []
    1.42    end
    1.43  
    1.44 @@ -396,7 +396,7 @@
    1.45        end
    1.46  
    1.47      val _ = List.app do_feat goal_feats
    1.48 -    val _ = rev_sort_array_prefix (Real.compare o pairself snd) num_facts overlaps_sqr
    1.49 +    val _ = sort_array_suffix (Real.compare o pairself snd) num_facts overlaps_sqr
    1.50      val no_recommends = Unsynchronized.ref 0
    1.51      val recommends = Array.tabulate (num_facts, rpair 0.0)
    1.52      val age = Unsynchronized.ref 500000000.0
    1.53 @@ -438,7 +438,7 @@
    1.54      while1 ();
    1.55      while2 ();
    1.56      select_visible_facts 1000000000.0 recommends visible_facts;
    1.57 -    rev_sort_array_prefix (Real.compare o pairself snd) max_suggs recommends;
    1.58 +    sort_array_suffix (Real.compare o pairself snd) max_suggs recommends;
    1.59      ret [] (Integer.max 0 (num_facts - max_suggs))
    1.60    end
    1.61  
    1.62 @@ -1126,7 +1126,7 @@
    1.63  val extra_feature_factor = 0.1 (* FUDGE *)
    1.64  val num_extra_feature_facts = 10 (* FUDGE *)
    1.65  
    1.66 -val max_proximity_facts = 100
    1.67 +val max_proximity_facts = 100 (* FUDGE *)
    1.68  
    1.69  fun find_mash_suggestions ctxt max_facts suggs facts chained raw_unknown =
    1.70    let