--- a/src/Pure/drule.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/drule.ML Fri Jul 15 15:44:15 2005 +0200
@@ -958,8 +958,8 @@
(* vars in left-to-right order *)
-fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
-fun vars_of_terms ts = rev (Library.foldl Term.add_vars ([], ts));
+fun tvars_of_terms ts = rev (fold Term.add_tvars ts []);
+fun vars_of_terms ts = rev (fold Term.add_vars ts []);
fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm];
fun vars_of thm = vars_of_terms [Thm.full_prop_of thm];