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:10 2012 +0200
     1.3 @@ -119,7 +119,7 @@
     1.4       SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
     1.5       SELECT_GOAL (Local_Defs.unfold_tac ctxt
     1.6         (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
     1.7 -     TRY o rtac (mk_UnIN pp jj), (*#####*)
     1.8 +     rtac (mk_UnIN pp jj),
     1.9       atac ORELSE'
    1.10       rtac @{thm singletonI} ORELSE'
    1.11       (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'