src/HOL/Tools/datatype_package.ML
changeset 13466 42766aa25460
parent 13462 56610e2ba220
child 13480 bb72bd43c6c3
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Aug 07 16:43:41 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Aug 07 16:44:47 2002 +0200
     1.3 @@ -590,7 +590,8 @@
     1.4        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
     1.5        add_cases_induct dt_infos induct |>
     1.6        Theory.parent_path |>
     1.7 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
     1.8 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
     1.9 +      DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.10    in
    1.11      (thy12,
    1.12       {distinct = distinct,
    1.13 @@ -646,7 +647,8 @@
    1.14        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.15        add_cases_induct dt_infos induct |>
    1.16        Theory.parent_path |>
    1.17 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
    1.18 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.19 +      DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.20    in
    1.21      (thy12,
    1.22       {distinct = distinct,
    1.23 @@ -752,7 +754,8 @@
    1.24        put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
    1.25        add_cases_induct dt_infos induction' |>
    1.26        Theory.parent_path |>
    1.27 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms));
    1.28 +      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.29 +      DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    1.30    in
    1.31      (thy11,
    1.32       {distinct = distinct,