# HG changeset patch
# User wenzelm
# Date 954535179 -7200
# Node ID 40036a2ab64608c8465a209582c15d522dc39c27
# Parent  c47735e7bd1c85728e96e547d1b013876f682125
use cong_add_global att;

diff -r c47735e7bd1c -r 40036a2ab646 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Mar 31 22:39:06 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 31 22:39:39 2000 +0200
@@ -529,7 +529,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), [Simplifier.change_global_ss (op addcongs)])]) |>
+        (("", weak_case_congs), [cong_add_global])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;