src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 51160 599ff65b85e2
parent 51126 df86080de4cb
child 51998 f732a674db1b
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 15:22:16 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Feb 15 11:47:33 2013 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4  fun multi_base_blacklist ctxt ho_atp =
     1.5    ["defs", "select_defs", "update_defs", "split", "splits", "split_asm",
     1.6     "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong",
     1.7 -   "weak_case_cong", "nibble_pair_of_char_simps", "nibble.simps",
     1.8 +   "weak_case_cong", "nat_of_char_simps", "nibble.simps",
     1.9     "nibble.distinct"]
    1.10    |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ?
    1.11          append ["induct", "inducts"]