--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Oct 01 20:38:57 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Tue Oct 02 01:00:18 2012 +0200
@@ -109,9 +109,9 @@
fun mk_corec_like_tac corec_like_defs map_ids'' ctor_dtor_corec_like pre_map_def ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
- (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN
- unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN
- (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1;
+ (rtac (ctor_dtor_corec_like RS trans) THEN' asm_simp_tac ss_if_True_False) 1 THEN_MAYBE
+ (unfold_thms_tac ctxt (pre_map_def :: @{thm id_def} :: sum_prod_thms_map @ map_ids'') THEN
+ (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong)) 1);
fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =
EVERY (map3 (fn case_split_tac => fn corec_like_thm => fn disc =>