src/HOL/Tools/ATP/atp_proof_reconstruct.ML

         val props =
           Symtab.empty
           |> 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 =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
                @{term False}