1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Jun 29 16:17:55 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Jun 29 16:17:56 2009 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4    val the_info : theory -> string -> info
     1.5    val the_descr : theory -> string list
     1.6      -> descr * (string * sort) list * string list
     1.7 -      * (string list * string list) * (typ list * typ list)
     1.8 +      * string * (string list * string list) * (typ list * typ list)
     1.9    val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
    1.10    val get_constrs : theory -> string -> (string * typ) list option
    1.11    val get_all : theory -> info Symtab.table
    1.12 @@ -125,9 +125,10 @@
    1.13  
    1.14      val names = map Long_Name.base_name (the_default tycos (#alt_names info));
    1.15      val (auxnames, _) = Name.make_context names
    1.16 -      |> fold_map (yield_singleton Name.variants o name_of_typ) Us
    1.17 +      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
    1.18 +    val prefix = space_implode "_" names;
    1.19  
    1.20 -  in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
    1.21 +  in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
    1.22  
    1.23  fun get_constrs thy dtco =
    1.24    case try (the_spec thy) dtco