src/HOL/Tools/Metis/metis_translate.ML

         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
                             false false props @{prop False} []
 (*
 val _ = tracing ("ATP PROBLEM: " ^ cat_lines (tptp_strings_for_atp_problem CNF atp_problem))
 *)
+      (* "rev" is for compatibility *)
       val axioms =
         atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
+                    |> rev
     in
       (mode, sym_tab, {axioms = axioms, tfrees = [], old_skolems = old_skolems})
     end
   | prepare_metis_problem ctxt mode conj_clauses fact_clauses =
     let