changeset 16787 | b6b6e2faaa41 |
parent 16536 | c5744af6b28a |
child 16880 | 411d91d104c4 |
--- a/src/Pure/proofterm.ML Wed Jul 13 10:48:21 2005 +0200 +++ b/src/Pure/proofterm.ML Wed Jul 13 11:16:34 2005 +0200 @@ -766,8 +766,8 @@ (***** axioms and theorems *****) -fun vars_of t = rev (foldl_aterms - (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t)); +fun vars_of t = rev (fold_aterms + (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []); fun test_args _ [] = true | test_args is (Bound i :: ts) =