1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 23:09:08 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 23:42:33 2012 +0200
1.3 @@ -28,12 +28,10 @@
1.4 rtac refl) 1;
1.5
1.6 fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
1.7 - Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
1.8 - rtac sumEN' 1 THEN
1.9 + Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
1.10 Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
1.11 - EVERY' (map2 (fn k => fn m =>
1.12 - select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN' etac @{thm meta_mp}) k THEN'
1.13 - atac) (1 upto n) ms) 1;
1.14 + EVERY' (map2 (fn k => fn m => select_prem_tac n (REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
1.15 + etac @{thm meta_mp}) k THEN' atac) (1 upto n) ms) 1;
1.16
1.17 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
1.18 (rtac iffI THEN'
1.19 @@ -47,9 +45,7 @@
1.20 rtac @{thm sum.distinct(1)} 1;
1.21
1.22 fun mk_inject_tac ctxt ctr_def fld_inject =
1.23 - Local_Defs.unfold_tac ctxt [ctr_def] THEN
1.24 - rtac (fld_inject RS ssubst) 1 THEN
1.25 - Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN
1.26 - rtac refl 1;
1.27 + Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
1.28 + Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
1.29
1.30 end;