src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML

   let
     val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   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
     fun aux _ _ [] = []
       | aux n skolem_somes (th :: ths) =