src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

     val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} =
       smt_filter_loop name params state goal subgoal factss
     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) =
       (case outcome of
         NONE =>