src/HOL/Tools/datatype_rep_proofs.ML
changeset 13340 9b0332344ae2
parent 12922 ed70a600f0ea
child 13585 db4005b40cc6
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 16:54:07 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 18:35:34 2002 +0200
     1.3 @@ -639,20 +639,19 @@
     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 [InductivePackage.inductive_forall_def] (cert
     1.8 +    val dt_induct = prove_goalw_cterm [] (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             [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
    1.13              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    1.14              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
    1.15 -              rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
    1.16 +              dtac FunsD 1, etac CollectD 1]))]))
    1.17                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    1.18  
    1.19      val (thy7, [dt_induct']) = thy6 |>
    1.20        Theory.add_path big_name |>
    1.21 -      PureThy.add_thms [(("induct", dt_induct),
    1.22 -        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
    1.23 +      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    1.24        Theory.parent_path;
    1.25  
    1.26    in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')