explicit pointless checkpoint
authorhaftmann
Mon Sep 28 09:47:18 2009 +0200 (2009-09-28)
changeset 32722ad04cda866be
parent 32721 a5fcc7960681
child 32723 866cebde3fca
explicit pointless checkpoint
src/HOL/Tools/Datatype/datatype.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:58:25 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 09:47:18 2009 +0200
     1.3 @@ -345,8 +345,9 @@
     1.4      |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
     1.5    end;
     1.6  
     1.7 -fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 =
     1.8 +fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy1 =
     1.9    let
    1.10 +    val thy2 = thy1 |> Theory.checkpoint
    1.11      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
    1.12      val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    1.13      val (case_names_induct, case_names_exhausts) =
    1.14 @@ -403,7 +404,10 @@
    1.15        ||>> store_thmss "distinct" new_type_names raw_distinct
    1.16        ||> Sign.add_path (space_implode "_" new_type_names)
    1.17        ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
    1.18 -  in derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 end;
    1.19 +  in
    1.20 +    thy2
    1.21 +    |> derive_datatype_props config dt_names alt_names descr sorts induct inject distinct
    1.22 + end;
    1.23  
    1.24  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.25    let