| changeset 16787 | b6b6e2faaa41 |
| parent 16720 | 0c6c67e74391 |
| child 16790 | be2780f435e1 |
--- a/src/Pure/drule.ML Wed Jul 13 10:48:21 2005 +0200 +++ b/src/Pure/drule.ML Wed Jul 13 11:16:34 2005 +0200 @@ -958,7 +958,7 @@ (* vars in left-to-right order *) -fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts)); +fun tvars_of_terms ts = rev (fold 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];