# HG changeset patch
# User blanchet
# Date 1352201925 -3600
# Node ID 3f8ee43ac62f65d391e31323c7be68a454742753
# Parent  3bb634c9fedb3a7d69ca4aa7d4c63599f8c892ac
removed needless sort

diff -r 3bb634c9fedb -r 3f8ee43ac62f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 11:24:48 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 12:38:45 2012 +0100
@@ -814,9 +814,9 @@
       end
     val sum_up_time =
       Vector.foldl
-      ((fn (SOME t, (b, s)) => (b, t + s)
-         | (NONE, (_, s)) => (true, preplay_timeout + s)) o apfst Lazy.force)
-      (false, seconds 0.0)
+        ((fn (SOME t, (b, s)) => (b, t + s)
+           | (NONE, (_, s)) => (true, preplay_timeout + s)) o apfst Lazy.force)
+        (false, seconds 0.0)
 
     (* Metis Preplaying *)
     fun try_metis timeout (Prove (_, _, t, By_Metis fact_names)) =
@@ -891,10 +891,9 @@
             val refed_by = refed_by |> fold
               (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs
             val new_candidates =
-              fold
-                (fn (i, [_]) => cons (cost (get i proof_vect |> the), i) | _ => I)
+              fold (fn (i, [_]) => cons (cost (get i proof_vect |> the), i)
+                     | _ => I)
                 (map (fn i => (i, get i refed_by)) refs) []
-              |> sort cand_ord
             val cand_tab = add_list cand_tab new_candidates
             val proof_vect = proof_vect |> replace NONE i |> replace s j
           in