1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 15:50:26 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 29 16:11:02 2010 +0200
     1.3 @@ -382,16 +382,14 @@
     1.4          val (x, ty_args) =
     1.5            case head of
     1.6              CombConst (name as (s, s'), _, ty_args) =>
     1.7 -            if top_level then
     1.8 -              if s = "equal" then
     1.9 -                (if length args = 2 then name
    1.10 -                 else ("c_fequal", @{const_name fequal}), [])
    1.11 -              else if s = "c_False" then
    1.12 -                (("$false", s'), [])
    1.13 -              else if s = "c_True" then
    1.14 -                (("$true", s'), [])
    1.15 -              else
    1.16 -                (name, if full_types then [] else ty_args)
    1.17 +            if s = "equal" then
    1.18 +              (if top_level andalso length args = 2 then name
    1.19 +               else ("c_fequal", @{const_name fequal}), [])
    1.20 +            else if top_level then
    1.21 +              case s of
    1.22 +                "c_False" => (("$false", s'), [])
    1.23 +              | "c_True" => (("$true", s'), [])
    1.24 +              | _ => (name, if full_types then [] else ty_args)
    1.25              else
    1.26                (name, if full_types then [] else ty_args)
    1.27            | CombVar (name, _) => (name, [])