1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 12:40:48 2011 +0200
     1.3 @@ -949,7 +949,8 @@
     1.4                 combformula
     1.5  fun add_nonmonotonic_types_for_facts ctxt type_sys facts =
     1.6    level_of_type_sys type_sys = Nonmonotonic_Types
     1.7 -  ? (insert_type I @{typ bool} (* in case helper "True_or_False" is included *)
     1.8 +  (* in case helper "True_or_False" is included (FIXME) *)
     1.9 +  ? (insert_type I @{typ bool}
    1.10       #> fold (add_fact_nonmonotonic_types ctxt) facts)
    1.11  
    1.12  fun n_ary_strip_type 0 T = ([], T)