# HG changeset patch # User blanchet # Date 1305206959 -7200 # Node ID 2490e5e2f3f50568d7641d99392746a9f645982d # Parent d6db5a8154770e56ee991b31680b80a52626cedf gracefully declare fTrue and fFalse proxies' types if the constants only appear in the helpers diff -r d6db5a815477 -r 2490e5e2f3f5 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 @@ -908,9 +908,9 @@ combformula fun add_nonmonotonic_types_for_facts ctxt type_sys facts = level_of_type_sys type_sys = Nonmonotonic_Types - (* in case helper "True_or_False" is included (FIXME) *) - ? (insert_type I @{typ bool} - #> fold (add_fact_nonmonotonic_types ctxt) facts) + ? (fold (add_fact_nonmonotonic_types ctxt) facts + (* in case helper "True_or_False" is included *) + #> insert_type I @{typ bool}) fun n_ary_strip_type 0 T = ([], T) | n_ary_strip_type n (Type (@{type_name fun}, [dom_T, ran_T])) = @@ -1033,7 +1033,7 @@ val helpers = repaired_sym_tab |> helper_facts_for_sym_table ctxt type_sys |> map repair val sym_decl_lines = - (conjs, facts) (* FIXME: what if "True_or_False" is among helpers? *) + (conjs, helpers @ facts) |> sym_decl_table_for_facts type_sys repaired_sym_tab |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys (* Reordering these might confuse the proof reconstruction code or the SPASS