# HG changeset patch
# User haftmann
# Date 1256019031 -7200
# Node ID 94108ea8c568d884e4f9c639f880524417090584
# Parent  cda9a931a46bc5b8b4bee3faff7791b911f6974a
more accurate checkpoints

diff -r cda9a931a46b -r 94108ea8c568 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Mon Oct 19 16:34:12 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 08:10:31 2009 +0200
@@ -403,14 +403,12 @@
       in (thm', lthy') end;
     fun tac thms = Class.intro_classes_tac []
       THEN ALLGOALS (ProofContext.fact_tac thms);
-    fun add_eq_thms dtco thy =
-      let
-        val (thms, thm) = mk_eq_eqns thy dtco
-      in
-        thy
-        |> Code.add_nbe_eqn thm
-        |> fold_rev Code.add_eqn thms
-      end;
+    fun add_eq_thms dtco =
+      Theory.checkpoint
+      #> `(fn thy => mk_eq_eqns thy dtco)
+      #-> (fn (thms, thm) =>
+        Code.add_nbe_eqn thm
+        #> fold_rev Code.add_eqn thms);
   in
     thy
     |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
@@ -418,7 +416,6 @@
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
     |-> (fn def_thms => fold Code.del_eqn def_thms)
-    |> Theory.checkpoint
     |> fold add_eq_thms dtcos
   end;