# HG changeset patch
# User wenzelm
# Date 1244717318 -7200
# Node ID a6c6bf2751a096e17fb3869c326b5a937a118cae
# Parent  39746cae148dd13bf2a6752befd9764daa789b57
added sporadic (Local)Theory.checkpoint, to enable parallel proof checking;

diff -r 39746cae148d -r a6c6bf2751a0 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Thu Jun 11 11:21:01 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Thu Jun 11 12:48:38 2009 +0200
@@ -802,6 +802,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
@@ -1052,7 +1053,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
@@ -1345,7 +1346,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'
@@ -1359,6 +1360,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
@@ -1417,7 +1419,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)
@@ -1425,7 +1427,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 **)
@@ -1446,6 +1448,7 @@
     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')
     val _ = Output.tracing ("preds: " ^ commas preds)