# HG changeset patch
# User desharna
# Date 1605703474 -3600
# Node ID 4eea17b3ac5851c2798199fb71b39cf55aac9bff
# Parent  fffad9ad660efac8de637c5ae327277f1989126e
Tuned parentheses in TPTP output

diff -r fffad9ad660e -r 4eea17b3ac58 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Nov 17 23:26:41 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Nov 18 13:44:34 2020 +0100
@@ -370,6 +370,10 @@
   | is_format_typed (DFG _) = true
   | is_format_typed _ = false
 
+fun is_format_with_fool (THF (With_FOOL, _, _)) = true
+  | is_format_with_fool (TFF (With_FOOL, _)) = true
+  | is_format_with_fool _ = false
+
 fun tptp_string_of_role Axiom = "axiom"
   | tptp_string_of_role Definition = "definition"
   | tptp_string_of_role Lemma = "lemma"
@@ -465,7 +469,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 ? parens
+        |> (is_format_higher_order format orelse is_format_with_fool format) ? parens
       else if s = tptp_ho_forall orelse s = tptp_ho_exists then
         (case ts of
           [AAbs (((s', ty), tm), [])] =>