# HG changeset patch
# User blanchet
# Date 1280412662 -7200
# Node ID a9847fb539dd430d68bad4881b9aa932b8f5ecfc
# Parent  dddb8ba3a1ce62fd5a2f7fcfd2d324d3982d1a0a
fix bug with "=" vs. "fequal" introduced by last change (dddb8ba3a1ce)

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 = "~"
diff -r dddb8ba3a1ce -r a9847fb539dd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:50:26 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 16:11:02 2010 +0200
@@ -382,16 +382,14 @@
         val (x, ty_args) =
           case head of
             CombConst (name as (s, s'), _, ty_args) =>
-            if top_level then
-              if s = "equal" then
-                (if length args = 2 then name
-                 else ("c_fequal", @{const_name fequal}), [])
-              else if s = "c_False" then
-                (("$false", s'), [])
-              else if s = "c_True" then
-                (("$true", s'), [])
-              else
-                (name, if full_types then [] else ty_args)
+            if s = "equal" then
+              (if top_level andalso length args = 2 then name
+               else ("c_fequal", @{const_name fequal}), [])
+            else if top_level then
+              case s of
+                "c_False" => (("$false", s'), [])
+              | "c_True" => (("$true", s'), [])
+              | _ => (name, if full_types then [] else ty_args)
             else
               (name, if full_types then [] else ty_args)
           | CombVar (name, _) => (name, [])