--- 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 = "~"