--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 28 19:34:08 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
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 28 18:39:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 28 19:34:08 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 =
--- a/src/Pure/Isar/local_theory.ML Sun Mar 28 18:39:27 2010 +0200
+++ b/src/Pure/Isar/local_theory.ML Sun Mar 28 19:34:08 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 ());