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