src/HOL/Tools/datatype_rep_proofs.ML
changeset 18314 4595eb4627fa
parent 17985 d5d576b72371
child 18330 444f16d232a2
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 06:28:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 08:28:02 2005 +0100
     1.3 @@ -16,8 +16,8 @@
     1.4    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     1.5      string list -> DatatypeAux.descr list -> (string * sort) list ->
     1.6        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
     1.7 -        -> theory -> theory * thm list list * thm list list * thm list list *
     1.8 -          DatatypeAux.simproc_dist list * thm
     1.9 +        -> theory -> (thm list list * thm list list * thm list list *
    1.10 +          DatatypeAux.simproc_dist list * thm) * theory
    1.11  end;
    1.12  
    1.13  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    1.14 @@ -577,9 +577,11 @@
    1.15      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
    1.16        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
    1.17  
    1.18 -    val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
    1.19 -      store_thmss "inject" new_type_names constr_inject |>>>
    1.20 -      store_thmss "distinct" new_type_names distinct_thms;
    1.21 +    val ((constr_inject', distinct_thms'), thy6) =
    1.22 +      thy5
    1.23 +      |> parent_path flat_names
    1.24 +      |> store_thmss "inject" new_type_names constr_inject
    1.25 +      ||>> store_thmss "distinct" new_type_names distinct_thms;
    1.26  
    1.27      (*************************** induction theorem ****************************)
    1.28  
    1.29 @@ -642,7 +644,8 @@
    1.30        PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.31        Theory.parent_path;
    1.32  
    1.33 -  in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
    1.34 +  in
    1.35 +    ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
    1.36    end;
    1.37  
    1.38  end;