diff -r 54b5df610651 -r b6b6e2faaa41 src/Pure/proofterm.ML
--- 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) =