src/HOL/Library/refute.ML

     (* for ALL types, not ...)                                             *)
     val _ = null (Term.add_tvars t []) orelse
       error "Term to be refuted contains schematic type variables"
 
     (* existential closure over schematic variables *)
-    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
+    val vars = sort_by (fst o fst) (Term.add_vars t [])
     (* Term.term *)
     val ex_closure = fold (fn ((x, i), T) => fn t' =>
       HOLogic.exists_const T $
         Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
     (* Note: If 't' is of type 'propT' (rather than 'boolT'), applying   *)