--- 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;