diff -r b605ebd87a47 -r f9908452b282 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Nov 19 11:04:53 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun Nov 21 11:21:16 2021 +0100
@@ -393,6 +393,10 @@
 
 fun is_format_higher_order (THF _) = true
   | is_format_higher_order _ = false
+
+fun is_format_higher_order_with_choice (THF (_, _, THF_With_Choice)) = true
+  | is_format_higher_order_with_choice _ = false
+
 fun is_format_typed (TFF _) = true
   | is_format_typed (THF _) = true
   | is_format_typed (DFG _) = true
@@ -519,7 +523,7 @@
             if ts = [] orelse is_format_higher_order format then
               app0 (s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")") [] ts
             else
-              error (tptp_let ^ " is special syntax and more than three arguments is only \
+              error (tptp_let ^ " is special syntax and more than two arguments is only \
                 \supported in higher order")
           end
         | _ => error (tptp_let ^ " is special syntax and must have at least two arguments"))
@@ -529,19 +533,21 @@
           if ts = [] orelse is_format_higher_order format then
             app0 (s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")") [] ts
           else
-            error (tptp_ite ^" is special syntax and more than three arguments is only supported \
+            error (tptp_ite ^ " is special syntax and more than three arguments is only supported \
               \in higher order")
-        | _ => error "$ite is special syntax and must have at least three arguments")
+        | _ => error (tptp_ite ^ " is special syntax and must have at least three arguments"))
       else if s = tptp_choice then
         (case ts of
-          [AAbs (((s', ty), tm), args)] =>
+          (AAbs (((s', ty), tm), args) :: ts) =>
           (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
              abstraction. *)
-          tptp_string_of_app format
-              (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^
-               "]: " ^ of_term tm ^ ""
-               |> parens) (map of_term args)
-        | _ => app ())
+          if ts = [] orelse is_format_higher_order_with_choice format then
+            let val declaration = s' ^ " : " ^ of_type ty in
+              app0 ("(" ^ tptp_choice ^ "[" ^ declaration ^ "]: " ^ of_term tm ^ ")") [] (args @ ts)
+            end
+          else
+            error (tptp_choice ^ " is only supported in higher order")
+        | _ => error (tptp_choice ^ " must be followed by a lambda abstraction"))
       else
         (case (Symtab.lookup tptp_builtins s, ts) of
           (SOME {arity = 1, is_predicate = true}, [t]) =>