diff -r 3abda3c76df9 -r 124193c26751 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 17 14:37:16 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Aug 17 16:46:43 2010 +0200
@@ -63,12 +63,12 @@
   | string_for_connective AIff = "<=>"
   | string_for_connective ANotIff = "<~>"
 fun string_for_formula (AQuant (q, xs, phi)) =
-    string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
-    string_for_formula phi
+    "(" ^ string_for_quantifier q ^ "[" ^ commas xs ^ "] : " ^
+    string_for_formula phi ^ ")"
   | string_for_formula (AConn (ANot, [AAtom (ATerm ("equal", ts))])) =
     space_implode " != " (map string_for_term ts)
   | string_for_formula (AConn (c, [phi])) =
-    string_for_connective c ^ " " ^ string_for_formula phi
+    "(" ^ string_for_connective c ^ " " ^ string_for_formula phi ^ ")"
   | string_for_formula (AConn (c, phis)) =
     "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
                         (map string_for_formula phis) ^ ")"