src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 57983 6edc3529bb4e
parent 57963 cb67fac9bd89
child 58011 bc6bced136e5
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -190,7 +190,7 @@
     1.4  (* FIXME: put other record thms here, or declare as "no_atp" *)
     1.5  fun multi_base_blacklist ctxt ho_atp =
     1.6    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
     1.7 -   "eq.refl", "nchotomy", "case_cong", "weak_case_cong", "nat_of_char_simps", "nibble.simps",
     1.8 +   "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps",
     1.9     "nibble.distinct"]
    1.10    |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
    1.11    |> map (prefix Long_Name.separator)