# HG changeset patch
# User blanchet
# Date 1648551030 -7200
# Node ID cf09060add1c37a73b03eb31918fa26a60f1cb05
# Parent  4b8da5eef9d0b3d061242762b89a6ff5468b3d03
nicer TPTP output

diff -r 4b8da5eef9d0 -r cf09060add1c src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 29 08:06:07 2022 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 29 12:50:30 2022 +0200
@@ -253,7 +253,7 @@
 val tptp_hilbert_the = "@-"
 val tptp_not_infix = "!"
 val tptp_equal = "="
-val tptp_not_equal = "!="
+val tptp_not_equal = tptp_not_infix ^ tptp_equal
 val tptp_old_equal = "equal"
 val tptp_false = "$false"
 val tptp_true = "$true"
@@ -569,12 +569,14 @@
     |> parens
   | tptp_string_of_formula format
         (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) =
-    space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
-                  (map (tptp_string_of_term format) ts)
+    space_implode (" " ^ tptp_not_equal ^ " ") (map (tptp_string_of_term format) ts)
+    |> is_format_higher_order format ? parens
+  | 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
   | tptp_string_of_formula format (AConn (c, [phi])) =
-    tptp_string_of_connective c ^ " " ^
-    (tptp_string_of_formula format phi |> parens)
+    tptp_string_of_connective c ^ " " ^ (tptp_string_of_formula format phi |> parens)
     |> parens
   | tptp_string_of_formula format (AConn (c, phis)) =
     space_implode (" " ^ tptp_string_of_connective c ^ " ")