changeset 36543 | 0e7fc5bf38de |
parent 36532 | fdfc37254090 |
child 36635 | 080b755377c0 |
child 36641 | 83d4e01ebda5 |
--- a/src/HOL/HOL.thy Thu Apr 29 22:08:57 2010 +0200 +++ b/src/HOL/HOL.thy Thu Apr 29 22:56:32 2010 +0200 @@ -1491,7 +1491,7 @@ setup {* Induct.setup #> Context.theory_map (Induct.map_simpset (fn ss => ss - setmksimps (Simpdata.mksimps Simpdata.mksimps_pairs #> + 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}))) addsimprocs