# HG changeset patch
# User wenzelm
# Date 967503359 -7200
# Node ID 79db0e5b782430790234961a34f7e566fd2c351a
# Parent  2c5b42311eb0eb7ac7b1a8fc2d0361bfca651fc9
Simplifier.cong_add_global;

diff -r 2c5b42311eb0 -r 79db0e5b7824 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:31 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 29 00:55:59 2000 +0200
@@ -562,7 +562,7 @@
       (#1 o PureThy.add_thmss [(("simps", simps), []),
         (("", flat case_thms @ size_thms @ rec_thms), [Simplifier.simp_add_global]),
         (("", flat (inject @ distinct)), [iff_add_global]),
-        (("", weak_case_congs), [cong_add_global])]) |>
+        (("", weak_case_congs), [Simplifier.cong_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path |>