diff -r dacd9a08f0a3 -r a64a8f7d593e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 17 21:36:13 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Nov 19 10:53:22 2021 +0100
@@ -685,26 +685,11 @@
           (case try (unsuffix "_arith") s of
             SOME s => (true, s)
           | NONE => (false, s))
-        val (with_let, s) =
-          (case try (unsuffix "_let") s of
-            SOME s => (true, s)
-          | NONE => (false, s))
-        val (with_ite, s) =
-          (case try (unsuffix "_ite") s of
-            SOME s => (true, s)
-          | NONE => (false, s))
-        val syntax = {with_ite = with_ite, with_let = with_let}
+        val syntax = {with_ite = true, with_let = true}
         val (fool, core) =
           (case try (unsuffix "_fool") s of
             SOME s => (With_FOOL syntax, s)
           | NONE => (Without_FOOL, s))
-
-        fun validate_syntax (type_enc as Native (_, Without_FOOL, _, _)) =
-            if with_ite orelse with_let then
-              error "\"ite\" and \"let\" options require \"native_fool\" or \"native_higher\"."
-            else
-              type_enc
-          | validate_syntax type_enc = type_enc
       in
         (case (core, poly) of
           ("native", SOME poly) =>
@@ -728,7 +713,6 @@
            | (poly as Raw_Polymorphic _, All_Types) =>
              Native (Higher_Order THF_With_Choice, With_FOOL syntax, poly, All_Types)
            | _ => raise Same.SAME))
-        |> validate_syntax
       end
 
     fun nonnative_of_string core =