# HG changeset patch
# User wenzelm
# Date 951940153 -3600
# Node ID 80855ae484ce35060802bb9617a55910811bf8ee
# Parent  df7dccddc3de5614447f6d79ab1a01e9edc42d81
project induct rule;

diff -r df7dccddc3de -r 80855ae484ce src/HOL/Tools/datatype_package.ML
--- 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;