1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 16:57:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -97,10 +97,17 @@
     1.4         etac @{thm induct_set_step}) THEN'
     1.5      atac ORELSE' SELECT_GOAL (auto_tac ctxt);
     1.6  
     1.7 +fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
     1.8 +
     1.9 +fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'}
    1.10 +  | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1
    1.11 +  | gen_UnIN_tac n k = gen_UN_comprehI_tac @{thm UnI2} THEN' gen_UnIN_tac (n - 1) (k - 1);
    1.12 +
    1.13  val induct_prem_prem_thms =
    1.14 -  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex UN_insert Un_assoc[symmetric] Un_empty_left
    1.15 -      Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv
    1.16 -      snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp sum_map.simps};
    1.17 +  @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    1.18 +      UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv
    1.19 +      image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    1.20 +      sum_map.simps};
    1.21  
    1.22  (* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
    1.23     delay them. *)
    1.24 @@ -114,8 +121,7 @@
    1.25         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    1.26       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.27         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    1.28 -     rtac (mk_UnIN pp jj) THEN' mk_induct_prem_prem_endgame_tac ctxt qq ORELSE'
    1.29 -       SELECT_GOAL (auto_tac ctxt)]) (rev ppjjqqkks)) 1;
    1.30 +     gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    1.31  
    1.32  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    1.33    let val r = length ppjjqqkks in