src/HOL/Tools/TFL/usyntax.ML

 fun dest_vtype (TVar x) = x
   | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
 
 val is_vartype = can dest_vtype;
 
-val type_vars  = map mk_prim_vartype o typ_tvars
+val type_vars  = map mk_prim_vartype o OldTerm.typ_tvars
 fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
 
 val alpha  = mk_vartype "'a"
 val beta   = mk_vartype "'b"
 

   in rev(add(tm,[]))
   end;
 
 
 
-val type_vars_in_term = map mk_prim_vartype o term_tvars;
+val type_vars_in_term = map mk_prim_vartype o OldTerm.term_tvars;
 
 
 
 (* Prelogic *)
 fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)