Added calls to add_dt_realizers.

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