# HG changeset patch # User blanchet # Date 1407152885 -7200 # Node ID c1ce4ef23be57f8663561393860485d000228ce2 # Parent e1a3d025552d95ed249870d5656bea0599ff8852 restored more sorting diff -r e1a3d025552d -r c1ce4ef23be5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Aug 04 13:16:18 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Mon Aug 04 13:48:05 2014 +0200 @@ -73,7 +73,7 @@ fun n_facts names = let val n = length names in string_of_int n ^ " fact" ^ plural_s n ^ - (if n > 0 then ": " ^ (names |> map fst |> space_implode " ") else "") + (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end fun print silent f = if silent then () else Output.urgent_message (f ()) @@ -160,7 +160,7 @@ (case test timeout (sup @ l0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) - (filter_used_facts true used_facts l0) + (filter_used_facts true used_facts l0) | _ => (case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => @@ -243,7 +243,7 @@ in (case used_facts of SOME used_facts => - {outcome = NONE, used_facts = used_facts, used_from = used_from, + {outcome = NONE, used_facts = sort_wrt fst used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} | NONE => result) end