# HG changeset patch
# User desharna
# Date 1636628528 -3600
# Node ID 32e95d996accbfdc3784ff16b2443515d46b913f
# Parent  570eae6e36b05ab5c2a0d6f9828844b1548e04d1
tuned generation of TPTP with $ite in function position

diff -r 570eae6e36b0 -r 32e95d996acc src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 11 11:42:04 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 11 12:02:08 2021 +0100
@@ -1268,8 +1268,7 @@
         end
       | intro top_level args (IConst (name as (s, _), T, T_args)) =
         let val argc = length args in
-          if has_ite andalso s = "c_If" andalso
-              (argc = 3 orelse is_type_enc_higher_order type_enc) then
+          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
             IConst (`I tptp_let, T, [])