src/HOL/Tools/datatype_package.ML
changeset 17412 e26cb20ef0cc
parent 17325 d9d50222808e
child 17521 0f1c48de39f5
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4  
     1.5  (** theory information about datatypes **)
     1.6  
     1.7 -val datatype_info = Symtab.curried_lookup o get_datatypes;
     1.8 +val datatype_info = Symtab.lookup o get_datatypes;
     1.9  
    1.10  fun datatype_info_err thy name = (case datatype_info thy name of
    1.11        SOME info => info
    1.12 @@ -681,7 +681,7 @@
    1.13        Theory.add_path (space_implode "_" new_type_names) |>
    1.14        add_rules simps case_thms size_thms rec_thms inject distinct
    1.15                  weak_case_congs Simplifier.cong_add_global |> 
    1.16 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    1.17 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.18        add_cases_induct dt_infos induct |>
    1.19        Theory.parent_path |>
    1.20        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.21 @@ -739,7 +739,7 @@
    1.22        Theory.add_path (space_implode "_" new_type_names) |>
    1.23        add_rules simps case_thms size_thms rec_thms inject distinct
    1.24                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.25 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    1.26 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.27        add_cases_induct dt_infos induct |>
    1.28        Theory.parent_path |>
    1.29        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    1.30 @@ -847,7 +847,7 @@
    1.31        Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    1.32        add_rules simps case_thms size_thms rec_thms inject distinct
    1.33                  weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> 
    1.34 -      put_datatypes (fold Symtab.curried_update dt_infos dt_info) |>
    1.35 +      put_datatypes (fold Symtab.update dt_infos dt_info) |>
    1.36        add_cases_induct dt_infos induction' |>
    1.37        Theory.parent_path |>
    1.38        (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>