src/HOL/Tools/datatype_package.ML
changeset 9714 79db0e5b7824
parent 9704 c2f2f70bbb60
child 9739 8470c4662685
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:31 2000 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:59 2000 +0200
     1.3 @@ -562,7 +562,7 @@
     1.4        (#1 o PureThy.add_thmss [(("simps", simps), []),
     1.5          (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
     1.6          (("", flat (inject @ distinct)), [iff_add_global]),
     1.7 -        (("", weak_case_congs), [cong_add_global])]) |>
     1.8 +        (("", weak_case_congs), [Simplifier.cong_add_global])]) |>
     1.9        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.10        add_cases_induct dt_infos |>
    1.11        Theory.parent_path |>