src/HOL/TPTP/atp_theory_export.ML

       facts
       |> map (fn ((_, loc), th) =>
                  ((Thm.get_name_hint th, loc),
                    th |> prop_of |> mono ? monomorphize_term ctxt))
       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true combsN false
-                             true [] @{prop False}
+                             false true [] @{prop False}
       |> #1
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt format)))
     val all_names = facts |> map (Thm.get_name_hint o snd)