src/HOL/Tools/datatype_package.ML
changeset 12708 31672377dadc
parent 12448 473cb9f9e237
child 12876 a70df1e5bf10
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jan 11 00:27:40 2002 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 11 00:28:24 2002 +0100
     1.3 @@ -40,8 +40,9 @@
     1.4         induction : thm,
     1.5         size : thm list,
     1.6         simps : thm list}
     1.7 -  val rep_datatype_i : string list option -> (thm * theory attribute list) list list ->
     1.8 -    (thm * theory attribute list) list list -> (thm * theory attribute list) -> theory -> theory *
     1.9 +  val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
    1.10 +    (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
    1.11 +    theory -> theory *
    1.12        {distinct : thm list list,
    1.13         inject : thm list list,
    1.14         exhaustion : thm list,