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