# HG changeset patch
# User blanchet
# Date 1306253063 -7200
# Node ID 347d5197896ea876d40ed0ad538f94f77f1caf0f
# Parent  6b39a2098ffd1deed0f7c4fd884501f06558b534
ensure that the argument of logical negation is enclosed in parentheses in THF mode

diff -r 6b39a2098ffd -r 347d5197896e src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 17:05:29 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue May 24 18:04:23 2011 +0200
@@ -197,18 +197,22 @@
          "")
 
 fun string_for_formula format (AQuant (q, xs, phi)) =
-    "(" ^ string_for_quantifier q ^
+    string_for_quantifier q ^
     "[" ^ commas (map (string_for_bound_var format) xs) ^ "] : " ^
-    string_for_formula format phi ^ ")"
+    string_for_formula format phi
+    |> enclose "(" ")"
   | string_for_formula format (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
     space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ")
                   (map (string_for_term format) ts)
     |> format = THF ? enclose "(" ")"
   | string_for_formula format (AConn (c, [phi])) =
-    "(" ^ string_for_connective c ^ " " ^ string_for_formula format phi ^ ")"
+    string_for_connective c ^ " " ^
+    (string_for_formula format phi |> format = THF ? enclose "(" ")")
+    |> enclose "(" ")"
   | string_for_formula format (AConn (c, phis)) =
-    "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
-                        (map (string_for_formula format) phis) ^ ")"
+    space_implode (" " ^ string_for_connective c ^ " ")
+                  (map (string_for_formula format) phis)
+    |> enclose "(" ")"
   | string_for_formula format (AAtom tm) = string_for_term format tm
 
 val default_source =
diff -r 6b39a2098ffd -r 347d5197896e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 17:05:29 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 24 18:04:23 2011 +0200
@@ -382,7 +382,7 @@
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
    arguments = fn _ => fn _ => fn timeout => fn _ =>
-     " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
+     "-t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
      ^ " -s " ^ the_system system_name system_versions,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @