--- a/src/HOL/Tools/Datatype/datatype_data.ML Sun Jan 10 18:09:11 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Jan 10 18:11:00 2010 +0100
@@ -341,7 +341,8 @@
((Binding.empty, flat inject), [iff_add]),
((Binding.empty, map (fn th => th RS notE) (flat distinct)),
[Classical.safe_elim NONE]),
- ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)])]
+ ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]),
+ ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])]
@ named_rules @ unnamed_rules)
|> snd
|> add_case_tr' case_names