--- a/src/HOL/Tools/datatype_package.ML Wed Mar 01 20:48:57 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Mar 01 20:49:13 2000 +0100
@@ -209,8 +209,13 @@
fun add_cases_induct infos =
let
- fun add (ths, (name, {induction, exhaustion, ...}: datatype_info)) =
- (("", induction), [InductMethod.induct_type_global name]) ::
+ fun proj _ 1 thm = thm
+ | proj i n thm =
+ (if i + 1 < n then (fn th => th RS conjunct1) else I)
+ (Library.funpow i (fn th => th RS conjunct2) thm)
+ |> Drule.standard;
+ fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
+ (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
(("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
in PureThy.add_thms (foldl add ([], infos)) end;