1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Jul 10 16:54:07 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Jul 10 18:35:34 2002 +0200
     1.3 @@ -548,7 +548,7 @@
     1.4        thy2 |>
     1.5        Theory.add_path (space_implode "_" new_type_names) |>
     1.6        PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
     1.7 -        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
     1.8 +        [case_names_induct])] |>>>
     1.9        PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
    1.10        (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
    1.11        Theory.parent_path |>>>

     2.1 --- a/src/HOL/Tools/datatype_prop.ML	Wed Jul 10 16:54:07 2002 +0200
     2.2 +++ b/src/HOL/Tools/datatype_prop.ML	Wed Jul 10 18:35:34 2002 +0200
     2.3 @@ -113,9 +113,8 @@
     2.4          fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
     2.5                (make_pred k T $ Free (s, T))
     2.6            | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
     2.7 -              (Const (InductivePackage.inductive_forall_name,
     2.8 -                  [T --> HOLogic.boolT] ---> HOLogic.boolT) $
     2.9 -                Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop;
    2.10 +              all T $ Abs ("x", T, HOLogic.mk_Trueprop
    2.11 +                (make_pred k U $ (Free (s, T') $ Bound 0)));
    2.12  
    2.13          val recs = filter is_rec_type cargs;
    2.14          val Ts = map (typ_of_dtyp descr' sorts) cargs;

     3.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 16:54:07 2002 +0200
     3.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Jul 10 18:35:34 2002 +0200
     3.3 @@ -639,20 +639,19 @@
     3.4        map (Free o apfst fst o dest_Var) Ps;
     3.5      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
     3.6  
     3.7 -    val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
     3.8 +    val dt_induct = prove_goalw_cterm [] (cert
     3.9        (DatatypeProp.make_ind descr sorts)) (fn prems =>
    3.10          [rtac indrule_lemma' 1, indtac rep_induct 1,
    3.11           EVERY (map (fn (prem, r) => (EVERY
    3.12             [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
    3.13              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    3.14              DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
    3.15 -              rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
    3.16 +              dtac FunsD 1, etac CollectD 1]))]))
    3.17                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    3.18  
    3.19      val (thy7, [dt_induct']) = thy6 |>
    3.20        Theory.add_path big_name |>
    3.21 -      PureThy.add_thms [(("induct", dt_induct),
    3.22 -        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
    3.23 +      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    3.24        Theory.parent_path;
    3.25  
    3.26    in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')