src/HOL/Tools/datatype_package.ML
changeset 18455 b293c1087f1d
parent 18451 5ff0244e25e8
child 18462 b67d423b5234
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Dec 21 15:19:16 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 21 17:00:57 2005 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4    val get_datatype : theory -> string -> ((string * sort) list * string list) option
     1.5    val get_datatype_cons : theory -> string * string -> typ list option
     1.6    val get_case_const_data : theory -> string -> (string * int) list option
     1.7 -  val get_all_datatype_cons : theory -> (string * string list) list
     1.8 +  val get_all_datatype_cons : theory -> (string * string) list
     1.9    val constrs_of : theory -> string -> term list option
    1.10    val case_const_of : theory -> string -> term option
    1.11    val weak_case_congs_of : theory -> thm list
    1.12 @@ -1003,9 +1003,9 @@
    1.13  
    1.14  fun get_all_datatype_cons thy =
    1.15    Symtab.fold (fn (dtco, _) => fold
    1.16 -    (fn co =>
    1.17 -      AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco))
    1.18 -    ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
    1.19 +    (fn co => cons (co, dtco))
    1.20 +      ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
    1.21 +
    1.22  
    1.23  
    1.24  (** package setup **)