src/HOL/Tools/datatype_rep_proofs.ML
changeset 7499 23e090051cb8
parent 7293 959e060f4a2f
child 7704 9a6783fdb9a5
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Sep 06 22:12:08 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Sep 07 10:40:58 1999 +0200
     1.3 @@ -570,7 +570,7 @@
     1.4          [rtac iffI 1,
     1.5           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
     1.6           dresolve_tac rep_congs 1, dtac box_equals 1,
     1.7 -         REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def],
     1.8 +         REPEAT (resolve_tac rep_thms 1), rewtac o_def,
     1.9           REPEAT (eresolve_tac inj_thms 1),
    1.10           REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
    1.11                    eresolve_tac inj_thms 1, atac 1]))])
    1.12 @@ -634,7 +634,7 @@
    1.13           EVERY (map (fn (prem, r) => (EVERY
    1.14             [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
    1.15              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    1.16 -            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def],
    1.17 +            DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
    1.18                rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
    1.19                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    1.20