# HG changeset patch
# User desharna
# Date 1739346495 -3600
# Node ID b97cea26d3a3805ba380561670848e0b2608a6a3
# Parent  5d57110da8eb787b2bbf4f1cc055ed4ee2dbe2e5# Parent  08475a3360a88bd7bbac25e599b8797ce9c356b7
merged

diff -r 5d57110da8eb -r b97cea26d3a3 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Feb 11 18:20:00 2025 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Feb 12 08:48:15 2025 +0100
@@ -569,12 +569,10 @@
     |> parens
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
-    |> is_format_higher_order format ? parens
+    parens (space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts))
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("equal" (* tptp_old_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
-    |> is_format_higher_order format ? parens
+    parens (space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts))
   | tptp_string_of_formula format (AConn (c, [phi])) =
     tptp_string_of_connective c ^ " " ^ (tptp_string_of_formula format phi |> parens)
     |> parens