Now returns theorems with correct names in derivations.
authorberghofe
Wed Mar 15 23:38:52 2000 +0100 (2000-03-15)
changeset 84795d327a46dc61
parent 8478 6053a5cd2881
child 8480 50266d517b0c
Now returns theorems with correct names in derivations.
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 15 23:38:19 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 15 23:38:52 2000 +0100
     1.3 @@ -577,9 +577,9 @@
     1.4      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
     1.5        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
     1.6  
     1.7 -    val thy6 = thy5 |> parent_path flat_names |>
     1.8 -      (#1 o store_thmss "inject" new_type_names constr_inject) |>
     1.9 -      (#1 o store_thmss "distinct" new_type_names distinct_thms);
    1.10 +    val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
    1.11 +      store_thmss "inject" new_type_names constr_inject |>>>
    1.12 +      store_thmss "distinct" new_type_names distinct_thms;
    1.13  
    1.14      (*************************** induction theorem ****************************)
    1.15  
    1.16 @@ -641,7 +641,7 @@
    1.17        PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.18        Theory.parent_path;
    1.19  
    1.20 -  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
    1.21 +  in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
    1.22    end;
    1.23  
    1.24  end;