# HG changeset patch
# User wenzelm
# Date 1010705304 -3600
# Node ID 31672377dadcb2d5959f9a4f6449a5730194f5db
# Parent  4013be8572c5b12ba1951046ce58484e0e477965
clarified IsarThy.apply_theorems_i;

diff -r 4013be8572c5 -r 31672377dadc src/HOL/Tools/datatype_package.ML
--- 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,
diff -r 4013be8572c5 -r 31672377dadc src/HOL/Tools/recdef_package.ML
--- 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