diff -r c143ad7811fc -r da1fdbfebd39 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jul 30 12:07:14 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Jul 30 15:09:25 2013 +0200
@@ -1118,12 +1118,12 @@
         val ctxt' = Proof_Context.init_global thy'
         val rules as ((intro, elim), _) =
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
-        in thy'
+        in
+          thy'
           |> set_function_name Pred name mode mode_cname
           |> add_predfun_data name mode (definition, rules)
           |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "I"), intro) |> snd
           |> Global_Theory.store_thm (Binding.name (mode_cbasename ^ "E"), elim)  |> snd
-          |> Theory.checkpoint
         end;
   in
     thy |> defined_function_of Pred name |> fold create_definition modes
@@ -1366,8 +1366,7 @@
     val _ = print_step options "Defining executable functions..."
     val thy'' =
       cond_timeit (Config.get ctxt Quickcheck.timing) "Defining executable functions..."
-      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
-      |> Theory.checkpoint)
+      (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy')
     val ctxt'' = Proof_Context.init_global thy''
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
@@ -1388,7 +1387,7 @@
       fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib])] thy))
-      result_thms' thy'' |> Theory.checkpoint)
+      result_thms' thy'')
   in
     thy'''
   end
@@ -1397,7 +1396,7 @@
   let
     fun dest_steps (Steps s) = s
     val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
-    val thy' = extend_intro_graph names thy |> Theory.checkpoint;
+    val thy' = extend_intro_graph names thy;
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.restrict (member (op =) (Graph.all_succs gr keys)) gr)
     val scc = strong_conn_of (PredData.get thy') names
@@ -1414,7 +1413,7 @@
             add_equations_of steps mode_analysis_options options preds thy
           end
         else thy)
-      scc thy'' |> Theory.checkpoint
+      scc thy''
   in thy''' end
 
 val add_equations = gen_add_equations