--- 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