src/HOL/Library/refute.ML

--- a/src/HOL/Library/refute.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/HOL/Library/refute.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -1156,7 +1156,7 @@
       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 $