# HG changeset patch # User wenzelm # Date 1269796852 -7200 # Node ID 5d79ca55a52b70030a16935eb2b5b34e295da2ce # Parent f4f34350024925abf2672fca574066317605dbae implicit checkpoint in Local_Theory.theory as well -- no longer export Local_Theory.checkpoint; diff -r f4f343500249 -r 5d79ca55a52b src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 28 17:43:09 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 28 19:20:52 2010 +0200 @@ -170,7 +170,6 @@ if (is_inductify options) then let val lthy' = Local_Theory.theory (preprocess options t) lthy - |> Local_Theory.checkpoint val const = case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of SOME c => c diff -r f4f343500249 -r 5d79ca55a52b src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 28 17:43:09 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 28 19:20:52 2010 +0200 @@ -2912,7 +2912,6 @@ val const = prep_const thy raw_const val lthy' = Local_Theory.theory (PredData.map (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy - |> Local_Theory.checkpoint val thy' = ProofContext.theory_of lthy' val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy') fun mk_cases const = diff -r f4f343500249 -r 5d79ca55a52b src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Sun Mar 28 17:43:09 2010 +0200 +++ b/src/Pure/Isar/local_theory.ML Sun Mar 28 19:20:52 2010 +0200 @@ -20,7 +20,6 @@ val target_of: local_theory -> Proof.context val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val raw_theory: (theory -> theory) -> local_theory -> local_theory - val checkpoint: local_theory -> local_theory val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory val theory: (theory -> theory) -> local_theory -> local_theory val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory @@ -149,7 +148,8 @@ thy |> Sign.map_naming (K (naming_of lthy)) |> f - ||> Sign.restore_naming thy); + ||> Sign.restore_naming thy + ||> Theory.checkpoint); fun theory f = #2 o theory_result (f #> pair ());