# HG changeset patch
# User berghofe
# Date 953159932 -3600
# Node ID 5d327a46dc61de25370c8b7ef8907ff05b8d1a4e
# Parent  6053a5cd2881dd2ca5721cb31566716f49aa2147
Now returns theorems with correct names in derivations.

diff -r 6053a5cd2881 -r 5d327a46dc61 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 15 23:38:19 2000 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Mar 15 23:38:52 2000 +0100
@@ -577,9 +577,9 @@
     val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
 
-    val thy6 = thy5 |> parent_path flat_names |>
-      (#1 o store_thmss "inject" new_type_names constr_inject) |>
-      (#1 o store_thmss "distinct" new_type_names distinct_thms);
+    val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
+      store_thmss "inject" new_type_names constr_inject |>>>
+      store_thmss "distinct" new_type_names distinct_thms;
 
     (*************************** induction theorem ****************************)
 
@@ -641,7 +641,7 @@
       PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
       Theory.parent_path;
 
-  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
+  in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
   end;
 
 end;