| changeset 16790 | be2780f435e1 |
| parent 16787 | b6b6e2faaa41 |
| child 16861 | 7446b4be013b |
--- a/src/Pure/drule.ML Wed Jul 13 11:29:08 2005 +0200 +++ b/src/Pure/drule.ML Wed Jul 13 11:30:37 2005 +0200 @@ -958,7 +958,7 @@ (* vars in left-to-right order *) -fun tvars_of_terms ts = rev (fold Term.add_tvars ts []); +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 thm = tvars_of_terms [Thm.full_prop_of thm];