# HG changeset patch
# User berghofe
# Date 1028731487 -7200
# Node ID 42766aa25460c7aa108a5bd799c6131b5a400518
# Parent  08e3fe248ba9c2c3c5c98226625d4f828c7b0660
Added calls to add_dt_realizers.

diff -r 08e3fe248ba9 -r 42766aa25460 src/HOL/Tools/datatype_package.ML
--- 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,