src/HOL/Tools/datatype_package.ML
changeset 21127 c8e862897d13
parent 21045 66d6d1b0ddfa
child 21187 16fb5afbf228
--- a/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:14 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:16 2006 +0100
@@ -305,13 +305,14 @@
       
 fun add_rules simps case_thms size_thms rec_thms inject distinct
                   weak_case_congs cong_att =
-  (snd o PureThy.add_thmss [(("simps", simps), []),
+  PureThy.add_thmss [(("simps", simps), []),
     (("", flat case_thms @ size_thms @ 
           flat distinct @ rec_thms), [Simplifier.simp_add]),
-    (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
-    (("", flat inject),               [iff_add]),
-    (("", map name_notE (flat distinct)),  [Classical.safe_elim NONE]),
-    (("", weak_case_congs),                  [cong_att])]);
+    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
+    (("", flat inject), [iff_add]),
+    (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
+    (("", weak_case_congs), [cong_att])]
+  #> snd;
 
 
 (* add_cases_induct *)