diff -r 7384b771805d -r 77c432fe28ff src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:36 2011 +0200
@@ -376,8 +376,10 @@
 (*
 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