# HG changeset patch
# User blanchet
# Date 1349132418 -7200
# Node ID 00290dc6bfade5edee121ab6fce4e4a37e7bc530
# Parent  835d55b4fc8ceccd9172e3896b8aab222ac3d5ee
made (co)rec tactic more robust when the simplifier succeeds early

diff -r 835d55b4fc8c -r 00290dc6bfad src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- 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 =>