src/HOL/Tools/refute.ML

         (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
         superclasses
       (* replace the (at most one) schematic type variable in each axiom *)
       (* by the actual type 'T'                                          *)
       val monomorphic_class_axioms = map (fn (axname, ax) =>
-        (case Term.term_tvars ax of
+        (case Term.add_tvars ax [] of
           [] =>
           (axname, ax)
         | [(idx, S)] =>
           (axname, monomorphic_term (Vartab.make [(idx, (S, T))]) ax)
         | _ =>

 (*               return function types, set types, non-recursive IDTs, or    *)
 (*               'propT'.  For IDTs, also the argument types of constructors *)
 (*               and all mutually recursive IDTs are considered.             *)
 (* ------------------------------------------------------------------------- *)
 
-  (* theory -> Term.term -> Term.typ list *)
-
   fun ground_types thy t =
   let
-    (* Term.typ * Term.typ list -> Term.typ list *)
-    fun collect_types (T, acc) =
+    fun collect_types T acc =
       (case T of
-        Type ("fun", [T1, T2]) => collect_types (T1, collect_types (T2, acc))
+        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
       | Type ("prop", [])      => acc
-      | Type ("set", [T1])     => collect_types (T1, acc)
+      | Type ("set", [T1])     => collect_types T1 acc
       | Type (s, Ts)           =>
         (case DatatypePackage.get_datatype thy s of
           SOME info =>  (* inductive datatype *)
           let
             val index        = #index info

             let
               val dT = typ_of_dtyp descr typ_assoc d
             in
               case d of
                 DatatypeAux.DtTFree _ =>
-                collect_types (dT, acc)
+                collect_types dT acc
               | DatatypeAux.DtType (_, ds) =>
-                collect_types (dT, foldr collect_dtyp acc ds)
+                collect_types dT (foldr collect_dtyp acc ds)
               | DatatypeAux.DtRec i =>
                 if dT mem acc then
                   acc  (* prevent infinite recursion *)
                 else
                   let

             collect_dtyp (DatatypeAux.DtRec index, acc)
           end
         | NONE =>
           (* not an inductive datatype, e.g. defined via "typedef" or *)
           (* "typedecl"                                               *)
-          insert (op =) T (foldr collect_types acc Ts))
+          insert (op =) T (fold collect_types Ts acc))
       | TFree _                => insert (op =) T acc
       | TVar _                 => insert (op =) T acc)
   in
-    it_term_types collect_types (t, [])
+    fold_types collect_types t []
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* string_of_typ: (rather naive) conversion from types to strings, used to   *)
 (*                look up the size of a type in 'sizes'.  Parameterized      *)

   let
     (* disallow schematic type variables, since we cannot properly negate  *)
     (* terms containing them (their logical meaning is that there EXISTS a *)
     (* type s.t. ...; to refute such a formula, we would have to show that *)
     (* for ALL types, not ...)                                             *)
-    val _ = null (term_tvars t) orelse
+    val _ = null (Term.add_tvars t []) orelse
       error "Term to be refuted contains schematic type variables"
 
     (* existential closure over schematic variables *)
     (* (Term.indexname * Term.typ) list *)
     val vars = sort_wrt (fst o fst) (map dest_Var (OldTerm.term_vars t))