# 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), [])] =>