# HG changeset patch
# User desharna
# Date 1628178196 -7200
# Node ID b9837b07684d867ba85d5d9fd2fe116e5a552f95
# Parent  94c27a7a0d39ce9406705ec15ca2999148397f76
fixed $ite syntax in TPTP THX generation

diff -r 94c27a7a0d39 -r b9837b07684d src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 05 13:44:33 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 05 17:43:16 2021 +0200
@@ -501,6 +501,10 @@
             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)] =>