--- a/src/HOL/Tools/datatype_aux.ML Thu Sep 25 19:15:50 2008 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Thu Sep 25 20:34:15 2008 +0200
@@ -78,8 +78,8 @@
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
#> PureThy.add_thmss [((label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)
- ) (tnames ~~ attss ~~ thmss);
+ #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ ##> Theory.checkpoint;
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
@@ -87,8 +87,8 @@
fold_map (fn ((tname, atts), thms) =>
Sign.add_path tname
#> PureThy.add_thms [((label, thms), atts)]
- #-> (fn thm::_ => Sign.parent_path #> pair thm)
- ) (tnames ~~ attss ~~ thmss);
+ #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss)
+ ##> Theory.checkpoint;
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);