changeset 16787 | b6b6e2faaa41 |
parent 16486 | 1a12cdb6ee6b |
child 16790 | be2780f435e1 |
--- a/src/Pure/Proof/extraction.ML Wed Jul 13 10:48:21 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Jul 13 11:16:34 2005 +0200 @@ -128,8 +128,8 @@ fun msg d s = priority (Symbol.spaces d ^ s); -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 vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);