--- a/src/HOL/Tools/Datatype/rep_datatype.ML Tue Jul 30 12:07:14 2013 +0200
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Tue Jul 30 15:09:25 2013 +0200
@@ -149,8 +149,7 @@
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
(map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
- ||> Sign.restore_naming thy0
- ||> Theory.checkpoint;
+ ||> Sign.restore_naming thy0;
(* prove uniqueness and termination of primrec combinators *)
@@ -238,8 +237,7 @@
(Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
(set $ Free ("x", T) $ Free ("y", T')))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
- ||> Sign.parent_path
- ||> Theory.checkpoint;
+ ||> Sign.parent_path;
(* prove characteristic equations for primrec combinators *)
@@ -262,7 +260,6 @@
|> Global_Theory.note_thmss ""
[((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
||> Sign.parent_path
- ||> Theory.checkpoint
|-> (fn thms => pair (reccomb_names, maps #2 thms))
end;
@@ -325,8 +322,7 @@
|> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
in (defs @ [def_thm], thy') end)
- (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1)
- ||> Theory.checkpoint;
+ (hd descr ~~ newTs ~~ case_names ~~ take (length newTs) reccomb_names) ([], thy1);
val case_thms =
(map o map) (fn t =>
@@ -479,9 +475,8 @@
in
-fun derive_datatype_props config dt_names descr induct inject distinct thy1 =
+fun derive_datatype_props config dt_names descr induct inject distinct thy2 =
let
- val thy2 = thy1 |> Theory.checkpoint;
val flat_descr = flat descr;
val new_type_names = map Long_Name.base_name dt_names;
val _ =