--- a/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Tue Jan 16 00:33:40 2001 +0100
@@ -238,7 +238,8 @@
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
val (tac, _) = foldl mk_unique_tac
- ((rtac induct' 1, rec_intrs), descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
+ (((rtac induct' THEN_ALL_NEW atomize_strip_tac) 1, rec_intrs),
+ descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
in split_conj_thm (prove_goalw_cterm []
(cert (HOLogic.mk_Trueprop (mk_conj rec_unique_ts))) (K [tac]))
--- a/src/HOL/Tools/datatype_package.ML Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Jan 16 00:33:40 2001 +0100
@@ -532,7 +532,8 @@
val (thy3, (([induct], [rec_thms]), inject)) =
thy2 |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
+ PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
+ [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
(if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
Theory.parent_path |>>>
--- a/src/HOL/Tools/datatype_prop.ML Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_prop.ML Tue Jan 16 00:33:40 2001 +0100
@@ -113,8 +113,9 @@
fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
(make_pred k T $ Free (s, T))
| mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
- HOLogic.mk_Trueprop (HOLogic.all_const T $
- Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0)));
+ (Const (InductivePackage.inductive_forall_name,
+ [T --> HOLogic.boolT] ---> HOLogic.boolT) $
+ Abs ("x", T, make_pred k U $ (Free (s, T') $ Bound 0))) |> HOLogic.mk_Trueprop;
val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Jan 16 00:33:40 2001 +0100
@@ -626,7 +626,7 @@
map (Free o apfst fst o dest_Var) Ps;
val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
- val dt_induct = prove_goalw_cterm [] (cert
+ val dt_induct = prove_goalw_cterm [InductivePackage.inductive_forall_def] (cert
(DatatypeProp.make_ind descr sorts)) (fn prems =>
[rtac indrule_lemma' 1, indtac rep_induct 1,
EVERY (map (fn (prem, r) => (EVERY
@@ -638,7 +638,8 @@
val (thy7, [dt_induct']) = thy6 |>
Theory.add_path big_name |>
- PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
+ PureThy.add_thms [(("induct", dt_induct),
+ [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>
Theory.parent_path;
in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')