# HG changeset patch
# User blanchet
# Date 1282061721 -7200
# Node ID dafcd0d19b1138efa135845adc58b6b2d8c708df
# Parent  bb30e2f6fb0ea557cb22eac1c628235a3abb8a46
repair translation of "c_fequal"

diff -r bb30e2f6fb0e -r dafcd0d19b11 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 17 18:14:50 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Aug 17 18:15:21 2010 +0200
@@ -267,16 +267,18 @@
         val (x, ty_args) =
           case head of
             CombConst (name as (s, s'), _, 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)
+            let val ty_args = if full_types then [] else ty_args in
+              if s = "equal" then
+                if top_level andalso length args = 2 then (name, [])
+                else (("c_fequal", @{const_name fequal}), ty_args)
+              else if top_level then
+                case s of
+                  "c_False" => (("$false", s'), [])
+                | "c_True" => (("$true", s'), [])
+                | _ => (name, ty_args)
+              else
+                (name, ty_args)
+            end
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t = ATerm (x, map fo_term_for_combtyp ty_args @