src/HOL/Tools/refute.ML
changeset 44121 44adaa6db327
parent 43864 58a7b3fdc193
child 45387 ccffb3f9f42b
     1.1 --- a/src/HOL/Tools/refute.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4  fun close_form t =
     1.5    let
     1.6      (* (Term.indexname * Term.typ) list *)
     1.7 -    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
     1.8 +    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
     1.9    in
    1.10      fold (fn ((x, i), T) => fn t' =>
    1.11        Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
    1.12 @@ -1212,7 +1212,7 @@
    1.13  
    1.14      (* existential closure over schematic variables *)
    1.15      (* (Term.indexname * Term.typ) list *)
    1.16 -    val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))
    1.17 +    val vars = sort_wrt (fst o fst) (map dest_Var (Misc_Legacy.term_vars t))
    1.18      (* Term.term *)
    1.19      val ex_closure = fold (fn ((x, i), T) => fn t' =>
    1.20        HOLogic.exists_const T $