src/HOL/Tools/ATP/atp_problem.ML
changeset 78788 5a14f2cc1ea0
parent 77427 4cdefee3f97f
child 81624 6e09005f6ca8
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Oct 17 12:10:58 2023 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Oct 18 10:41:12 2023 +0200
@@ -493,7 +493,7 @@
         "[" ^ commas (map of_term ts) ^ "]"
       else if is_tptp_equal s then
         space_implode (" " ^ tptp_equal ^ " ") (map of_term ts)
-        |> (is_format_higher_order format orelse is_format_with_fool format) ? parens
+        |> (is_format_higher_order format orelse true) ? parens
       else if s = tptp_ho_forall orelse s = tptp_ho_exists then
         (case ts of
           [AAbs (((s', ty), tm), [])] =>