src/HOL/Tools/datatype_rep_proofs.ML
changeset 10911 eb5721204b38
parent 9315 f793f05024f6
child 11435 bd1a7f53c11b
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:32:38 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 16 00:33:40 2001 +0100
     1.3 @@ -626,7 +626,7 @@
     1.4        map (Free o apfst fst o dest_Var) Ps;
     1.5      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
     1.6  
     1.7 -    val dt_induct = prove_goalw_cterm [] (cert
     1.8 +    val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
     1.9        (DatatypeProp.make_ind descr sorts)) (fn prems =>
    1.10          [rtac indrule_lemma' 1, indtac rep_induct 1,
    1.11           EVERY (map (fn (prem, r) => (EVERY
    1.12 @@ -638,7 +638,8 @@
    1.13  
    1.14      val (thy7, [dt_induct']) = thy6 |>
    1.15        Theory.add_path big_name |>
    1.16 -      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.17 +      PureThy.add_thms [(("induct", dt_induct),
    1.18 +        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
    1.19        Theory.parent_path;
    1.20  
    1.21    in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')