src/HOL/Tools/datatype_package.ML
changeset 21127 c8e862897d13
parent 21045 66d6d1b0ddfa
child 21187 16fb5afbf228
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:14 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Oct 31 14:58:16 2006 +0100
     1.3 @@ -305,13 +305,14 @@
     1.4        
     1.5  fun add_rules simps case_thms size_thms rec_thms inject distinct
     1.6                    weak_case_congs cong_att =
     1.7 -  (snd o PureThy.add_thmss [(("simps", simps), []),
     1.8 +  PureThy.add_thmss [(("simps", simps), []),
     1.9      (("", flat case_thms @ size_thms @ 
    1.10            flat distinct @ rec_thms), [Simplifier.simp_add]),
    1.11 -    (("", size_thms @ rec_thms),             [setmp CodegenData.strict_functyp false (RecfunCodegen.add NONE)]),
    1.12 -    (("", flat inject),               [iff_add]),
    1.13 -    (("", map name_notE (flat distinct)),  [Classical.safe_elim NONE]),
    1.14 -    (("", weak_case_congs),                  [cong_att])]);
    1.15 +    (("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
    1.16 +    (("", flat inject), [iff_add]),
    1.17 +    (("", map name_notE (flat distinct)), [Classical.safe_elim NONE]),
    1.18 +    (("", weak_case_congs), [cong_att])]
    1.19 +  #> snd;
    1.20  
    1.21  
    1.22  (* add_cases_induct *)