src/Pure/Proof/proof_rewrite_rules.ML

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 10:48:21 2005 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 11:16:34 2005 +0200
@@ -210,8 +210,8 @@
 
 (**** eliminate definitions in proof ****)
 
-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 insert_refl defs Ts (prf1 %% prf2) =
       insert_refl defs Ts prf1 %% insert_refl defs Ts prf2