src/HOL/ex/predicate_compile.ML

         PureThy.add_defs false [((Binding.name (Long_Name.base_name mode_id ^ "_def"), def), [])]
       val (intro, elim) = create_intro_elim_rule nparams mode definition mode_id funT (Const (name, T)) thy'
       in thy' |> add_predfun name mode (mode_id, definition, intro, elim)
         |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), intro) |> snd
         |> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elim)  |> snd
+        |> Theory.checkpoint
       end;
   in
     fold create_definition modes thy
   end;
 

   val index = find_index (fn s => s = pred) (#names (fst ind_result))
   val (_, T) = dest_Const (nth (#preds (snd ind_result)) index) *)
   val nargs = length (binder_types T) - nparams_of thy pred
   val pred_case_rule = singleton (ind_set_codegen_preproc thy)
     (preprocess_elim thy nargs (the_elim_of thy pred))
-  (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}])*)
+  (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm Predicate.memb_code}])*)
 in
   REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   THEN etac (predfun_elim_of thy pred mode) 1
   THEN etac pred_case_rule 1
   THEN (EVERY (map

     prepare_intrs thy prednames
   val _ = tracing "Infering modes..."
   val modes = infer_modes thy extra_modes arities param_vs clauses
   val _ = print_modes modes
   val _ = tracing "Defining executable functions..."
-  val thy' = fold (create_definitions preds nparams) modes thy
+  val thy' = fold (create_definitions preds nparams) modes thy |> Theory.checkpoint
   val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses
   val _ = tracing "Compiling equations..."
   val ts = compile_preds thy' all_vs param_vs (extra_modes @ modes) clauses'
   val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
   val pred_mode =

     prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
   val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
     [((Binding.qualify true (Long_Name.base_name name) (Binding.name "equation"), result_thms),
       [Attrib.attribute_i thy Code.add_default_eqn_attrib])] thy))
     (arrange ((map (fn ((name, _), _) => name) pred_mode) ~~ result_thms)) thy'
+    |> Theory.checkpoint
 in
   thy''
 end
 
 (* generation of case rules from user-given introduction rules *)

     (data, keys)
   end;
 
 fun add_equations name thy =
   let
-    val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy;
+    val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
     (*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
     fun strong_conn_of gr keys =
       Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
     val scc = strong_conn_of (PredData.get thy') [name]
     val thy'' = fold_rev
       (fn preds => fn thy =>
         if forall (null o modes_of thy) preds then add_equations_of preds thy else thy)
-      scc thy'
+      scc thy' |> Theory.checkpoint
   in thy'' end
 
 (** user interface **)
 
 local

   
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
     
     val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy
+      |> LocalTheory.checkpoint
     val thy' = ProofContext.theory_of lthy'
     val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
     
     fun mk_cases const =
       let

       in mk_casesrule lthy' nparams intros end
     val cases_rules = map mk_cases preds
     fun after_qed thms =
       LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const)
   in
-    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy
-    (* FIXME: expected the actual local_theory to be lthy'; but works with lthy ??*) 
+    Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'
   end;
 
 structure P = OuterParse
 
 in