src/HOL/Tools/datatype_package.ML
changeset 18462 b67d423b5234
parent 18455 b293c1087f1d
child 18518 3b1dfa53e64f
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 22 00:28:44 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 22 00:28:46 2005 +0100
     1.3 @@ -305,20 +305,20 @@
     1.4  fun add_cases_induct infos induction =
     1.5    let
     1.6      val n = length (HOLogic.dest_concls (Thm.concl_of induction));
     1.7 -    fun proj i thm =
     1.8 -      if n = 1 then thm
     1.9 -      else (if i + 1 < n then (fn th => th RS conjunct1) else I)
    1.10 -        (Library.funpow i (fn th => th RS conjunct2) thm)
    1.11 -        |> Drule.zero_var_indexes
    1.12 -        |> RuleCases.save thm;
    1.13 +    fun proj i = ProjectRule.project induction (i + 1);
    1.14  
    1.15      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    1.16 -      [(("", proj index induction), [InductAttrib.induct_type_global name]),
    1.17 +      [(("", proj index), [InductAttrib.induct_type_global name]),
    1.18         (("", exhaustion), [InductAttrib.cases_type_global name])];
    1.19      fun unnamed_rule i =
    1.20 -      (("", proj i induction), [InductAttrib.induct_type_global ""]);
    1.21 -    val rules = List.concat (map named_rules infos) @ map unnamed_rule (length infos upto n - 1);
    1.22 -  in snd o PureThy.add_thms rules end;
    1.23 +      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type_global ""]);
    1.24 +  in
    1.25 +    PureThy.add_thms
    1.26 +      (List.concat (map named_rules infos) @
    1.27 +        map unnamed_rule (length infos upto n - 1)) #> snd #>
    1.28 +    PureThy.add_thmss [(("inducts",
    1.29 +      map (proj #> standard #> RuleCases.save induction) (0 upto n - 1)), [])] #> snd
    1.30 +  end;
    1.31  
    1.32  
    1.33