1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:33 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:33 2013 +0100
     1.3 @@ -467,9 +467,8 @@
     1.4      map fst (take max_facts sels) @ take (max_facts - length sels) unks
     1.5    | mesh_facts fact_eq max_facts mess =
     1.6      let
     1.7 -      val mess =
     1.8 -        mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
     1.9 -      fun score_in fact (global_weight, ((sel_len, sels), unks)) =
    1.10 +      val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
    1.11 +      fun score_in fact (global_weight, (sels, unks)) =
    1.12          let
    1.13            fun score_at j =
    1.14              case try (nth sels) j of
    1.15 @@ -484,8 +483,7 @@
    1.16          end
    1.17        fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
    1.18        val facts =
    1.19 -        fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
    1.20 -             []
    1.21 +        fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
    1.22      in
    1.23        facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
    1.24              |> map snd |> take max_facts