diff -r 32a00ff29d1a -r fe5722fce758 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -99,7 +99,7 @@
 fun store_thmss_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
     Sign.add_path tname
-    #> PureThy.add_thmss [((Binding.name label, thms), atts)]
+    #> Global_Theory.add_thmss [((Binding.name label, thms), atts)]
     #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;
 
@@ -108,7 +108,7 @@
 fun store_thms_atts label tnames attss thmss =
   fold_map (fn ((tname, atts), thms) =>
     Sign.add_path tname
-    #> PureThy.add_thms [((Binding.name label, thms), atts)]
+    #> Global_Theory.add_thms [((Binding.name label, thms), atts)]
     #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
   ##> Theory.checkpoint;