1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:05:53 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 19:57:20 2012 +0200
     1.3 @@ -65,6 +65,7 @@
     1.4    Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
     1.5    subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
     1.6    Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
     1.7 -  Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
     1.8 +  Local_Defs.unfold_tac ctxt @{thms id_def} THEN
     1.9 +  (rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1;
    1.10  
    1.11  end;