diff -r dddb8ba3a1ce -r a9847fb539dd src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 29 15:50:26 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Jul 29 16:11:02 2010 +0200
@@ -49,9 +49,10 @@
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 fun string_for_term (ATerm (s, [])) = s
+  | string_for_term (ATerm ("equal", ts)) =
+    space_implode " = " (map string_for_term ts)
   | string_for_term (ATerm (s, ts)) =
-    if s = "equal" then space_implode " = " (map string_for_term ts)
-    else s ^ "(" ^ commas (map string_for_term ts) ^ ")"
+    s ^ "(" ^ commas (map string_for_term ts) ^ ")"
 fun string_for_quantifier AForall = "!"
   | string_for_quantifier AExists = "?"
 fun string_for_connective ANot = "~"