explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;

--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 25 19:15:50 2008 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Sep 25 20:34:15 2008 +0200
@@ -244,7 +244,8 @@
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
-      ||> parent_path flat_names;
+      ||> parent_path flat_names
+      ||> Theory.checkpoint;
 
 
     (* prove characteristic equations for primrec combinators *)
@@ -265,6 +266,7 @@
     |> Sign.add_path (space_implode "_" new_type_names)
     |> PureThy.add_thmss [(("recs", rec_thms), [])]
     ||> Sign.parent_path
+    ||> Theory.checkpoint
     |-> (fn thms => pair (reccomb_names, Library.flat thms))
   end;
 
@@ -327,7 +329,8 @@
 
         in (defs @ [def_thm], thy')
         end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
-          (Library.take (length newTs, reccomb_names)));
+          (Library.take (length newTs, reccomb_names)))
+      ||> Theory.checkpoint;
 
     val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))

--- 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) []);
 

--- a/src/HOL/Tools/function_package/size.ML	Thu Sep 25 19:15:50 2008 +0200
+++ b/src/HOL/Tools/function_package/size.ML	Thu Sep 25 20:34:15 2008 +0200
@@ -231,6 +231,7 @@
       thy
       |> Sign.root_path
       |> Sign.add_path prefix
+      |> Theory.checkpoint
       |> prove_size_thms info new_type_names
       |> Sign.restore_naming thy
   end;