changeset 25458 | ba8f5e4fa336 |
parent 24959 | 119793c84647 |
child 25495 | 98f3596bec44 |
--- a/src/HOL/Tools/datatype_package.ML Fri Nov 23 17:37:56 2007 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Nov 23 21:09:30 2007 +0100 @@ -557,7 +557,7 @@ val thy2' = thy (** new types **) - |> fold2 (fn (name, mx) => fn tvs => TypedefPackage.add_typedecls [(name, tvs, mx)]) + |> fold2 (fn (name, mx) => fn tvs => Typedecl.add (name, tvs, mx) #> snd) types_syntax tyvars |> add_path flat_names (space_implode "_" new_type_names)