# HG changeset patch
# User berghofe
# Date 939142573 -7200
# Node ID 64662aa3c1735f09bbfeb89ad8f649fc4b0ae392
# Parent  01386eb4eab02084c8e2a4fddd59db3d7ac88741
rep_datatype now stores theorems properly.

diff -r 01386eb4eab0 -r 64662aa3c173 src/HOL/Tools/datatype_package.ML
--- 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;