src/HOL/ex/predicate_compile.ML

--- a/src/HOL/ex/predicate_compile.ML	Thu Jun 11 21:37:26 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Jun 11 21:39:08 2009 +0200
@@ -858,6 +858,7 @@
       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
@@ -1072,7 +1073,7 @@
   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
@@ -1365,7 +1366,7 @@
   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'
@@ -1379,6 +1380,7 @@
     [((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
@@ -1424,7 +1426,7 @@
 
 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)
@@ -1432,7 +1434,7 @@
     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 **)
@@ -1455,6 +1457,7 @@
     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')
     
@@ -1467,8 +1470,7 @@
     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