--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 30 23:40:14 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 30 23:43:09 2010 +0200
@@ -342,8 +342,8 @@
((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, flat (distinct @ inject)), [Induct.add_simp_rule])]
- @ named_rules @ unnamed_rules)
+ ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+ named_rules @ unnamed_rules)
|> snd
|> add_case_tr' case_names
|> register dt_infos