--- a/src/HOL/Tools/datatype_package.ML Sat Jul 02 13:08:28 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Mon Jul 04 11:04:10 2005 +0200
@@ -286,10 +286,10 @@
(#1 o PureThy.add_thmss [(("simps", simps), []),
(("", List.concat case_thms @ size_thms @
List.concat distinct @ rec_thms), [Simplifier.simp_add_global]),
- (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+ (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
(("", List.concat inject), [iff_add_global]),
(("", List.concat distinct RL [notE]), [Classical.safe_elim_global]),
- (("", weak_case_congs), [cong_att])]);
+ (("", weak_case_congs), [cong_att])]);
(* add_cases_induct *)