1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 22:23:11 2012 +0200
1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 14 22:23:11 2012 +0200
1.3 @@ -113,22 +113,23 @@
1.4 val induct_prem_prem_thms_delayed =
1.5 @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
1.6
1.7 +(* TODO: Get rid of the "auto_tac" (or at least use a naked context) *)
1.8 fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
1.9 | mk_induct_prem_prem_endgame_tac ctxt qq =
1.10 REPEAT_DETERM_N qq o
1.11 (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
1.12 etac @{thm induct_set_step}) THEN'
1.13 - atac;
1.14 + atac ORELSE' SELECT_GOAL (auto_tac ctxt);
1.15
1.16 -(* TODO: Get rid of the "blast_tac" (or at least use a naked context) *)
1.17 fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
1.18 EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
1.19 - [rotate_tac (~ nn), select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1,(*###*) etac meta_mp,
1.20 - SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
1.21 + [select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1 (*FIXME: needed?*), etac meta_mp,
1.22 + SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* FIXME: ### why on a line of its own? *)
1.23 SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
1.24 SELECT_GOAL (Local_Defs.unfold_tac ctxt
1.25 (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
1.26 - rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE' blast_tac ctxt])
1.27 + rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
1.28 + SELECT_GOAL (auto_tac ctxt)])
1.29 (rev ixs)) 1;
1.30
1.31 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =