diff -r b147d01b8ebc -r ef3742657bc6 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 11:36:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Jun 23 12:43:09 2010 +0200
@@ -216,7 +216,7 @@
   in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
 
 fun make_axiom_clauses thy clauses =
-  ([], []) |> fold (add_axiom_clause thy) clauses |> snd
+  ([], []) |> fold_rev (add_axiom_clause thy) clauses |> snd
 
 fun make_conjecture_clauses thy =
   let