diff -r 40eea08c0cc5 -r 1111a9a328fe src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- 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) =