--- 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*)