# HG changeset patch
# User blanchet
# Date 1360242333 -3600
# Node ID 211a9240b1e3faab4188b430e6166b44e78393f1
# Parent  7327a847f0c73b9e58f664b179499f9bb905e522
killed deadcode

diff -r 7327a847f0c7 -r 211a9240b1e3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:33 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 14:05:33 2013 +0100
@@ -467,9 +467,8 @@
     map fst (take max_facts sels) @ take (max_facts - length sels) unks
   | mesh_facts fact_eq max_facts mess =
     let
-      val mess =
-        mess |> map (apsnd (apfst (normalize_scores max_facts #> `length)))
-      fun score_in fact (global_weight, ((sel_len, sels), unks)) =
+      val mess = mess |> map (apsnd (apfst (normalize_scores max_facts)))
+      fun score_in fact (global_weight, (sels, unks)) =
         let
           fun score_at j =
             case try (nth sels) j of
@@ -484,8 +483,7 @@
         end
       fun weight_of fact = mess |> map_filter (score_in fact) |> scaled_avg
       val facts =
-        fold (union fact_eq o map fst o take max_facts o snd o fst o snd) mess
-             []
+        fold (union fact_eq o map fst o take max_facts o fst o snd) mess []
     in
       facts |> map (`weight_of) |> sort (int_ord o swap o pairself fst)
             |> map snd |> take max_facts