# 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 =