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>\undefined\, 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