Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authordesharna
Wed, 12 Feb 2025 08:48:15 +0100
changeset 82136 b97cea26d3a3
parent 82134 5d57110da8eb (current diff)
parent 82135 08475a3360a8 (diff)
child 82137 7281e57085ab
merged
--- 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
isabelle