src/HOL/Tools/datatype_package.ML
changeset 19874 cc4b2b882e4c
parent 19841 f2fa72c13186
child 19925 3f9341831812
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:31 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 13 23:41:34 2006 +0200
     1.3 @@ -316,22 +316,20 @@
     1.4  
     1.5  (* add_cases_induct *)
     1.6  
     1.7 -fun add_cases_induct infos induction =
     1.8 +fun add_cases_induct infos induction thy =
     1.9    let
    1.10 -    val n = length (HOLogic.dest_concls (Thm.concl_of induction));
    1.11 -    fun proj i = ProjectRule.project induction (i + 1);
    1.12 +    val inducts = ProjectRule.projections (ProofContext.init thy) induction;
    1.13  
    1.14      fun named_rules (name, {index, exhaustion, ...}: datatype_info) =
    1.15 -      [(("", proj index), [InductAttrib.induct_type name]),
    1.16 +      [(("", nth inducts index), [InductAttrib.induct_type name]),
    1.17         (("", exhaustion), [InductAttrib.cases_type name])];
    1.18      fun unnamed_rule i =
    1.19 -      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
    1.20 +      (("", nth inducts i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
    1.21    in
    1.22 -    PureThy.add_thms
    1.23 +    thy |> PureThy.add_thms
    1.24        (List.concat (map named_rules infos) @
    1.25 -        map unnamed_rule (length infos upto n - 1)) #> snd #>
    1.26 -    PureThy.add_thmss [(("inducts",
    1.27 -      map (proj #> standard #> RuleCases.save induction) (0 upto n - 1)), [])] #> snd
    1.28 +        map unnamed_rule (length infos upto length inducts - 1)) |> snd
    1.29 +    |> PureThy.add_thmss [(("inducts", inducts), [])] |> snd
    1.30    end;
    1.31  
    1.32  
    1.33 @@ -801,7 +799,7 @@
    1.34        ||>> apply_theorems [raw_induction];
    1.35      val sign = Theory.sign_of thy1;
    1.36  
    1.37 -    val induction' = freezeT induction;
    1.38 +    val induction' = Thm.freezeT induction;
    1.39  
    1.40      fun err t = error ("Ill-formed predicate in induction rule: " ^
    1.41        Sign.string_of_term sign t);