# HG changeset patch
# User blanchet
# Date 1280411426 -7200
# Node ID dddb8ba3a1ce62fd5a2f7fcfd2d324d3982d1a0a
# Parent  c802b76d542f54a65aae6695c6d20f2a0c9a9d25
generate correct names for "$true" and "$false";
this was lost somewhere in the non-clausification

diff -r c802b76d542f -r dddb8ba3a1ce src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:37:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:50:26 2010 +0200
@@ -381,10 +381,17 @@
         val (head, args) = strip_combterm_comb u
         val (x, ty_args) =
           case head of
-            CombConst (name, _, ty_args) =>
-            if fst name = "equal" then
-              (if top_level andalso length args = 2 then name
-               else ("c_fequal", @{const_name fequal}), [])
+            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)
             else
               (name, if full_types then [] else ty_args)
           | CombVar (name, _) => (name, [])