# HG changeset patch
# User desharna
# Date 1629475077 -7200
# Node ID 304f22435bc7e7f710dcbfb36243a87ea57a04f5
# Parent  3f371ba2b4fc6270884713431170ad3c70998e17
fixed $ite syntax in TPTP TFX generation

diff -r 3f371ba2b4fc -r 304f22435bc7 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Aug 19 14:23:47 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Aug 20 17:57:57 2021 +0200
@@ -101,6 +101,7 @@
   val tptp_empty_list : string
   val tptp_unary_builtins : string list
   val tptp_binary_builtins : string list
+  val tptp_ternary_builtins : string list
   val dfg_individual_type : string
   val isabelle_info_prefix : string
   val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -266,6 +267,7 @@
 val tptp_unary_builtins = [tptp_not]
 val tptp_binary_builtins =
   [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+val tptp_ternary_builtins = [tptp_ite]
 
 val dfg_individual_type = "iii" (* cannot clash *)
 
diff -r 3f371ba2b4fc -r 304f22435bc7 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Aug 19 14:23:47 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Aug 20 17:57:57 2021 +0200
@@ -1528,7 +1528,8 @@
     (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
     (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
     (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
-    (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+    (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins)) @
+    (map (rpair (mk_sym_info true 3)) tptp_ternary_builtins)
     |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
       ? cons (prefixed_predicator_name, mk_sym_info true 1)
   end