diff -r 54b5df610651 -r b6b6e2faaa41 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -23,8 +23,8 @@
 val quiet_mode = ref true;
 fun message s = if !quiet_mode then () else writeln 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 forall_intr (t, prop) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)