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 @@ -118,18 +118,18 @@
     1.4      REPEAT_DETERM_N qq o
     1.5        (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
     1.6         etac @{thm induct_set_step}) THEN'
     1.7 -    (atac ORELSE' blast_tac ctxt);
     1.8 +    atac;
     1.9  
    1.10 -(* TODO: Get rid of the "blast_tac" *)
    1.11 +(* TODO: Get rid of the "blast_tac" (or at least use a naked context) *)
    1.12  fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =
    1.13    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.14 -    [rotate_tac (~ nn), select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1,(*###*) etac meta_mp,
    1.15 -     SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
    1.16 -     SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
    1.17 -     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.18 -       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.19 -     rtac (mk_UnIN pp jj),
    1.20 -     mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ixs)) 1;
    1.21 +      [rotate_tac (~ nn), select_prem_tac nn (dtac meta_spec) kk, rotate_tac ~1,(*###*) etac meta_mp,
    1.22 +       SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### 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 +    (rev ixs)) 1;
    1.28  
    1.29  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ixs =
    1.30    EVERY [mk_induct_prepare_prem_tac n m k,