--- 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 ^ " ")