src/HOL/Tools/Datatype/datatype_aux.ML
changeset 33243 17014b1b9353
parent 33042 ddf1f03a9ad9
child 33244 db230399f890
     1.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:19:31 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Tue Oct 27 17:34:00 2009 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4    val get_rec_types : descr -> (string * sort) list -> typ list
     1.5    val interpret_construction : descr -> (string * sort) list
     1.6      -> { atyp: typ -> 'a, dtyp: typ list -> int * bool -> string * typ list -> 'a }
     1.7 -    -> ((string * Term.typ list) * (string * 'a list) list) list
     1.8 +    -> ((string * typ list) * (string * 'a list) list) list
     1.9    val check_nonempty : descr list -> unit
    1.10    val unfold_datatypes : 
    1.11      theory -> descr -> (string * sort) list -> info Symtab.table ->