src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
changeset 57776 1111a9a328fe
parent 57750 670cbec816b9
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Mon Aug 04 11:54:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Mon Aug 04 12:28:42 2014 +0200
@@ -189,7 +189,7 @@
     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt2_filter_loop name params state goal subgoal factss
     val used_named_facts = map snd fact_ids
-    val used_facts = map fst used_named_facts
+    val used_facts = sort_wrt fst (map fst used_named_facts)
     val outcome = Option.map failure_of_smt2_failure outcome
 
     val (preferred_methss, message) =