src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 60924 610794dff23c
parent 60201 90e88e521e0e
child 62505 9e2a65912111
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -192,7 +192,7 @@
     val used_facts =
       (case fact_ids of
         NONE => map fst used_from
-      | SOME ids => sort_wrt fst (map (fst o snd) ids))
+      | SOME ids => sort_by fst (map (fst o snd) ids))
     val outcome = Option.map failure_of_smt_failure outcome
 
     val (preferred_methss, message) =