# 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