1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:11 2012 +0200
     1.3 @@ -112,12 +112,12 @@
     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 -fun mk_induct_prem_prem_endgame_tac ctxt qq =
     1.8 -  atac ORELSE'
     1.9 -  rtac @{thm singletonI} ORELSE'
    1.10 -  (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.11 -     etac @{thm induct_set_step}) THEN'
    1.12 -   (atac ORELSE' blast_tac ctxt));
    1.13 +fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    1.14 +  | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.15 +    REPEAT_DETERM_N qq o
    1.16 +      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    1.17 +       etac @{thm induct_set_step}) THEN'
    1.18 +    (atac ORELSE' blast_tac ctxt);
    1.19  
    1.20  (* TODO: Get rid of the "blast_tac" *)
    1.21  fun mk_induct_discharge_prem_prems_tac ctxt nn ixs set_natural's pre_set_defs =