src/HOL/Tools/datatype_package.ML

   val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
   val is_datatype : theory -> string -> bool
   val get_datatype : theory -> string -> ((string * sort) list * string list) option
   val get_datatype_cons : theory -> string * string -> typ list option
   val get_case_const_data : theory -> string -> (string * int) list option
-  val get_all_datatype_cons : theory -> (string * string list) list
+  val get_all_datatype_cons : theory -> (string * string) list
   val constrs_of : theory -> string -> term list option
   val case_const_of : theory -> string -> term option
   val weak_case_congs_of : theory -> thm list
   val setup: (theory -> theory) list
 end;

     | SOME (_, {index, descr, ...}) =>
         (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
 
 fun get_all_datatype_cons thy =
   Symtab.fold (fn (dtco, _) => fold
-    (fn co =>
-      AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco))
-    ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
+    (fn co => cons (co, dtco))
+      ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
+
 
 
 (** package setup **)
 
 (* setup theory *)