src/HOL/Tools/ATP/atp_problem.ML

               val definition = s' ^ " := " ^ of_term t1
               val usage = of_term tm
             in
             s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")"
             end
+        | _ => app ())
+      else if s = tptp_ite then
+        (case ts of
+          [t1, t2, t3] => s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")"
         | _ => app ())
       else if s = tptp_choice then
         (case ts of
           [AAbs (((s', ty), tm), args)] =>
           (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an