# 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