# HG changeset patch
# User blanchet
# Date 1648201547 -3600
# Node ID 28d2cb99b37f2dee06c12c5adbce2126ef069720
# Parent  4598cf29ef9880d5409b1c9600d144e3c36625fa
added parentheses in TPTP output -- seem necessary for some provers

diff -r 4598cf29ef98 -r 28d2cb99b37f src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Mar 24 23:54:40 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Mar 25 10:45:47 2022 +0100
@@ -583,8 +583,7 @@
     |> is_format_higher_order format ? parens
   | tptp_string_of_formula format (AConn (c, [phi])) =
     tptp_string_of_connective c ^ " " ^
-    (tptp_string_of_formula format phi
-     |> is_format_higher_order format ? parens)
+    (tptp_string_of_formula format phi |> parens)
     |> parens
   | tptp_string_of_formula format (AConn (c, phis)) =
     space_implode (" " ^ tptp_string_of_connective c ^ " ")