merged
authordesharna
Mon, 16 Aug 2021 23:07:01 +0200
changeset 74154 62b0577123a5
parent 74153 46f66e821f5c (diff)
parent 74152 069f6b2c5a07 (current diff)
child 74155 0faa68dedce5
child 74190 9a1796acd0a4
merged
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 16 11:49:39 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 16 23:07:01 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)] =>