src/Pure/Proof/extraction.ML
changeset 16790 be2780f435e1
parent 16787 b6b6e2faaa41
child 16800 90eff1b52428
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Jul 13 11:29:08 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 11:30:37 2005 +0200
     1.3 @@ -128,8 +128,8 @@
     1.4  
     1.5  fun msg d s = priority (Symbol.spaces d ^ s);
     1.6  
     1.7 -fun vars_of t = rev (fold_aterms
     1.8 -  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
     1.9 +fun vars_of t = rev (foldl_aterms
    1.10 +  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
    1.11  
    1.12  fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
    1.13