diff -r a5c2386518e2 -r fc26d5538868 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
@@ -897,7 +897,7 @@
           |> fold (fn Definition_Step _ => I (* FIXME *)
                     | Inference_Step ((s, _), t, _, _) =>
                       Symtab.update_new (s,
-                          t |> fold_rev forall_of (map Var (Term.add_vars t []))
+                          t |> fold forall_of (map Var (Term.add_vars t []))
                             |> member (op = o apsnd fst) tainted s ? s_not))
                   atp_proof
         fun prop_of_clause c =