# HG changeset patch
# User wenzelm
# Date 1269797648 -7200
# Node ID 3956a7636d5de10e1d90d5b1b28850622c3b2318
# Parent  eb44a5d40b9ef673698789f383344db82813abbe# Parent  5d79ca55a52b70030a16935eb2b5b34e295da2ce
merged

diff -r eb44a5d40b9e -r 3956a7636d5d src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- 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
diff -r eb44a5d40b9e -r 3956a7636d5d src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- 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 =
diff -r eb44a5d40b9e -r 3956a7636d5d src/Pure/Isar/local_theory.ML
--- 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 ());