diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -109,7 +109,7 @@
     fun add_eq_thms tyco =
       Theory.checkpoint
       #> `(fn thy => mk_eq_eqns thy tyco)
-      #-> (fn (thms, thm) => PureThy.note_thmss Thm.lemmaK
+      #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK
           [((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]),
             ((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])])
       #> snd