--- 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;