src/HOL/TPTP/atp_theory_export.ML

                                   Symtab.empty [] [] css_table
       |> sort (Sledgehammer_MaSh.crude_thm_ord o pairself snd)
     val problem =
       facts
       |> map (fn ((_, loc), th) =>
-                 ((Thm.get_name_hint th, loc),
-                   th |> prop_of |> mono ? monomorphize_term ctxt))
-      |> prepare_atp_problem ctxt format Axiom type_enc Exporter combsN false
-                             false true [] @{prop False}
+        ((Thm.get_name_hint th, loc), th |> prop_of |> mono ? monomorphize_term ctxt))
+      |> generate_atp_problem ctxt format Axiom type_enc Exporter combsN false false true []
+        @{prop False}
       |> #1 |> sort_wrt (heading_sort_key o fst)
     val prelude = fst (split_last problem)
     val name_tabs = Sledgehammer_Fact.build_name_tables Thm.get_name_hint facts
     val infers =
       if infer_policy = No_Inferences then