--- a/src/HOL/Tools/datatype_package.ML Fri Jan 11 00:27:40 2002 +0100
+++ b/src/HOL/Tools/datatype_package.ML Fri Jan 11 00:28:24 2002 +0100
@@ -40,8 +40,9 @@
induction : thm,
size : thm list,
simps : thm list}
- val rep_datatype_i : string list option -> (thm * theory attribute list) list list ->
- (thm * theory attribute list) list list -> (thm * theory attribute list) -> theory -> theory *
+ val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
+ (thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
+ theory -> theory *
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,