--- a/src/HOL/Tools/datatype_package.ML Wed Aug 07 16:43:41 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Aug 07 16:44:47 2002 +0200
@@ -590,7 +590,8 @@
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
+ (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
(thy12,
{distinct = distinct,
@@ -646,7 +647,8 @@
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
+ (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
(thy12,
{distinct = distinct,
@@ -752,7 +754,8 @@
put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
add_cases_induct dt_infos induction' |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
+ (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
(thy11,
{distinct = distinct,