added parentheses in TPTP output -- seem necessary for some provers
authorblanchet
Fri, 25 Mar 2022 10:45:47 +0100
changeset 75337 28d2cb99b37f
parent 75336 4598cf29ef98
child 75338 73034d385688
added parentheses in TPTP output -- seem necessary for some provers
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 ^ " ")