# HG changeset patch
# User haftmann
# Date 1254124038 -7200
# Node ID ad04cda866beabc79334c268386bc5bdca789e1b
# Parent  a5fcc7960681926aeb157ebaf5426231968dc483
explicit pointless checkpoint

diff -r a5fcc7960681 -r ad04cda866be src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:58:25 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 09:47:18 2009 +0200
@@ -345,8 +345,9 @@
     |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
   end;
 
-fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 =
+fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy1 =
   let
+    val thy2 = thy1 |> Theory.checkpoint
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
     val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
     val (case_names_induct, case_names_exhausts) =
@@ -403,7 +404,10 @@
       ||>> store_thmss "distinct" new_type_names raw_distinct
       ||> Sign.add_path (space_implode "_" new_type_names)
       ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
-  in derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 end;
+  in
+    thy2
+    |> derive_datatype_props config dt_names alt_names descr sorts induct inject distinct
+ end;
 
 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
   let