# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 54b3c9c056643d9cc9b9eca90cddb082fbf35a68
# Parent  d64956b03c70a7ca35086031d6cfbd57ab2cd84c
make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences

diff -r d64956b03c70 -r 54b3c9c05664 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -410,7 +410,13 @@
             CombConst (name as (s, s'), _, ty_args) =>
             (case AList.lookup (op =) fname_table s of
                SOME (n, fname) =>
-               (if top_level andalso length args = n then name else fname, [])
+               (if top_level andalso length args = n then
+                  case s of
+                    "c_False" => ("$false", s')
+                  | "c_True" => ("$true", s')
+                  | _ => name
+                else
+                  fname, [])
              | NONE =>
                case strip_prefix_and_unascii const_prefix s of
                  NONE => (name, ty_args)
@@ -419,15 +425,7 @@
                    val s'' = invert_const s''
                    val ty_args =
                      if needs_type_args thy type_sys s'' then ty_args else []
-                  in
-                    if top_level then
-                      case s of
-                        "c_False" => (("$false", s'), [])
-                      | "c_True" => (("$true", s'), [])
-                      | _ => (name, ty_args)
-                    else
-                      (name, ty_args)
-                  end)
+                  in (name, ty_args) end)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t =