# HG changeset patch
# User berghofe
# Date 1272968806 -7200
# Node ID 83d4e01ebda579e41574f91b619c18e4eb96cc1a
# Parent  25153c08655e2f2862841c86a83b7a91f5efaab6
induct_true_def and induct_false_def are already contained in induct_rulify_fallback.

diff -r 25153c08655e -r 83d4e01ebda5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon May 03 14:35:10 2010 +0200
+++ b/src/HOL/HOL.thy	Tue May 04 12:26:46 2010 +0200
@@ -1493,7 +1493,7 @@
   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"]