# HG changeset patch # User wenzelm # Date 1222367655 -7200 # Node ID 232fcbba2e4e83aa5d6cef88a4b45dd4808a960a # Parent cf3542e34726e22cee3fa0b0a28d21916914424b explicit checkpoint for low-level (global) theory operations, admits concurrent proofs; diff -r cf3542e34726 -r 232fcbba2e4e src/HOL/Tools/datatype_abs_proofs.ML --- 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]))) diff -r cf3542e34726 -r 232fcbba2e4e src/HOL/Tools/datatype_aux.ML --- 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) []); diff -r cf3542e34726 -r 232fcbba2e4e src/HOL/Tools/function_package/size.ML --- 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;