diff -r 32e95d996acc -r ef9f95d055f6 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 11 12:02:08 2021 +0100 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Nov 11 15:34:02 2021 +0100 @@ -1270,7 +1270,7 @@ let val argc = length args in if has_ite andalso s = "c_If" andalso argc >= 3 then IConst (`I tptp_ite, T, []) - else if is_fool andalso s = "c_Let" andalso argc = 2 then + else if is_fool andalso s = "c_Let" andalso argc >= 2 then IConst (`I tptp_let, T, []) else (case proxify_const s of