src/HOL/Library/refute.ML
changeset 60924 610794dff23c
parent 60190 906de96ba68a
child 61770 a20048c78891
     1.1 --- a/src/HOL/Library/refute.ML	Wed Aug 12 21:38:39 2015 +0200
     1.2 +++ b/src/HOL/Library/refute.ML	Thu Aug 13 11:05:19 2015 +0200
     1.3 @@ -1156,7 +1156,7 @@
     1.4        error "Term to be refuted contains schematic type variables"
     1.5  
     1.6      (* existential closure over schematic variables *)
     1.7 -    val vars = sort_wrt (fst o fst) (Term.add_vars t [])
     1.8 +    val vars = sort_by (fst o fst) (Term.add_vars t [])
     1.9      (* Term.term *)
    1.10      val ex_closure = fold (fn ((x, i), T) => fn t' =>
    1.11        HOLogic.exists_const T $