# HG changeset patch
# User blanchet
# Date 1304592048 -7200
# Node ID f4d17cc370f9d6652d22e34f01daa7734fc0f9d3
# Parent  d4f5fec71ded7ce358d1e363a7e9b27cf902b94a
added FIXME

diff -r d4f5fec71ded -r f4d17cc370f9 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
@@ -949,7 +949,8 @@
                combformula
 fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
   level_of_type_sys type_sys = Nonmonotonic_Types
-  ? (insert_type I @{typ bool} (* in case helper "True_or_False" is included *)
+  (* in case helper "True_or_False" is included (FIXME) *)
+  ? (insert_type I @{typ bool}
      #> fold (add_fact_nonmonotonic_types ctxt) facts)
 
 fun n_ary_strip_type 0 T = ([], T)