--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 23 22:07:55 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Nov 23 22:59:39 2011 +0100
@@ -355,7 +355,7 @@
((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.cong_add]),
((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
named_rules @ unnamed_rules)
|> snd