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