--- 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) ^ ")"