rep_datatype now stores theorems properly.

--- a/src/HOL/Tools/datatype_package.ML	Tue Oct 05 18:26:34 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Oct 05 18:56:13 1999 +0200
@@ -612,7 +612,10 @@
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
     val thy9 = thy8 |>
+      store_thmss "inject" new_type_names inject |>
+      store_thmss "distinct" new_type_names distinct |>
       Theory.add_path (space_implode "_" new_type_names) |>
+      PureThy.add_thms [(("induct", induction), [])] |>
       PureThy.add_thmss [(("simps", simps), [])] |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       Theory.parent_path;