diff -r 5c25a2012975 -r 0eade173f77e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Dec 31 15:30:10 2008 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Dec 31 18:53:16 2008 +0100
@@ -440,11 +440,11 @@
 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
 
 fun tvar_classes_of_terms ts =
-  let val sorts_list = map (map #2 o term_tvars) ts
+  let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
 
 fun tfree_classes_of_terms ts =
-  let val sorts_list = map (map #2 o term_tfrees) ts
+  let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   in  Symtab.keys (delete_type (foldl add_classes Symtab.empty sorts_list))  end;
 
 (*fold type constructors*)