1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 28 18:39:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 28 19:34:08 2010 +0200
     1.3 @@ -170,7 +170,6 @@
     1.4      if (is_inductify options) then
     1.5        let
     1.6          val lthy' = Local_Theory.theory (preprocess options t) lthy
     1.7 -          |> Local_Theory.checkpoint
     1.8          val const =
     1.9            case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
    1.10              SOME c => c

     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Mar 28 18:39:27 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Mar 28 19:34:08 2010 +0200
     2.3 @@ -2912,7 +2912,6 @@
     2.4      val const = prep_const thy raw_const
     2.5      val lthy' = Local_Theory.theory (PredData.map
     2.6          (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
     2.7 -      |> Local_Theory.checkpoint
     2.8      val thy' = ProofContext.theory_of lthy'
     2.9      val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
    2.10      fun mk_cases const =

     3.1 --- a/src/Pure/Isar/local_theory.ML	Sun Mar 28 18:39:27 2010 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Mar 28 19:34:08 2010 +0200
     3.3 @@ -20,7 +20,6 @@
     3.4    val target_of: local_theory -> Proof.context
     3.5    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     3.6    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     3.7 -  val checkpoint: local_theory -> local_theory
     3.8    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     3.9    val theory: (theory -> theory) -> local_theory -> local_theory
    3.10    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    3.11 @@ -149,7 +148,8 @@
    3.12      thy
    3.13      |> Sign.map_naming (K (naming_of lthy))
    3.14      |> f
    3.15 -    ||> Sign.restore_naming thy);
    3.16 +    ||> Sign.restore_naming thy
    3.17 +    ||> Theory.checkpoint);
    3.18  
    3.19  fun theory f = #2 o theory_result (f #> pair ());
    3.20