src/HOL/HOL.thy

 setup {*
   Induct.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
-        @{thms induct_rulify_fallback induct_true_def induct_false_def})))
+        @{thms induct_rulify_fallback})))
     addsimprocs
       [Simplifier.simproc @{theory} "swap_induct_false"
          ["induct_false ==> PROP P ==> PROP Q"]
          (fn _ => fn _ =>
             (fn _ $ (P as _ $ @{const induct_false}) $ (_ $ Q $ _) =>