--- 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,
--- a/src/HOL/Tools/recdef_package.ML Fri Jan 11 00:27:40 2002 +0100
+++ b/src/HOL/Tools/recdef_package.ML Fri Jan 11 00:28:24 2002 +0100
@@ -34,7 +34,7 @@
theory * {simps: thm list, rules: thm list list, induct: thm, tcs: term list}
val defer_recdef: xstring -> string list -> (xstring * Args.src list) list
-> theory -> theory * {induct_rules: thm}
- val defer_recdef_i: xstring -> term list -> (thm * theory attribute list) list
+ val defer_recdef_i: xstring -> term list -> (thm list * theory attribute list) list
-> theory -> theory * {induct_rules: thm}
val recdef_tc: bstring * Args.src list -> xstring -> int option
-> bool -> theory -> ProofHistory.T