src/ZF/Tools/datatype_package.ML
changeset 17412 e26cb20ef0cc
parent 17261 193b84a70ca4
child 17936 308b19d78764
     1.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -383,8 +383,8 @@
     1.4            (("recursor_eqns", recursor_eqns), []),
     1.5            (("free_iffs", free_iffs), []),
     1.6            (("free_elims", free_SEs), [])])
     1.7 -        |> DatatypesData.map (Symtab.curried_update (big_rec_name, dt_info))
     1.8 -        |> ConstructorsData.map (fold Symtab.curried_update con_pairs)
     1.9 +        |> DatatypesData.map (Symtab.update (big_rec_name, dt_info))
    1.10 +        |> ConstructorsData.map (fold Symtab.update con_pairs)
    1.11          |> Theory.parent_path,
    1.12     ind_result,
    1.13     {con_defs = con_defs,