src/HOL/Tools/datatype_package.ML
changeset 8325 80855ae484ce
parent 8306 9855f1801d2b
child 8405 0255394a05da
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Mar 01 20:48:57 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Mar 01 20:49:13 2000 +0100
     1.3 @@ -209,8 +209,13 @@
     1.4  
     1.5  fun add_cases_induct infos =
     1.6    let
     1.7 -    fun add (ths, (name, {induction, exhaustion, ...}: datatype_info)) =
     1.8 -      (("", induction), [InductMethod.induct_type_global name]) ::
     1.9 +    fun proj _ 1 thm = thm
    1.10 +      | proj i n thm =
    1.11 +          (if i + 1 < n then (fn th => th RS conjunct1) else I)
    1.12 +            (Library.funpow i (fn th => th RS conjunct2) thm)
    1.13 +          |> Drule.standard;
    1.14 +    fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
    1.15 +      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
    1.16         (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
    1.17    in PureThy.add_thms (foldl add ([], infos)) end;
    1.18