src/Pure/proofterm.ML
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) =