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