diff -r af605e186480 -r abf0f018b5ec src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Jan 14 17:20:51 2006 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Jan 14 22:25:34 2006 +0100
@@ -367,8 +367,8 @@
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Theory.add_path big_rec_base_name
         |> PureThy.add_thmss
-         [(("simps", simps), [Simplifier.simp_add_global]),
-          (("", intrs), [Classical.safe_intro_global]),
+         [(("simps", simps), [Attrib.theory Simplifier.simp_add]),
+          (("", intrs), [Attrib.theory Classical.safe_intro]),
           (("con_defs", con_defs), []),
           (("case_eqns", case_eqns), []),
           (("recursor_eqns", recursor_eqns), []),