# HG changeset patch
# User traytel
# Date 1348817887 -7200
# Node ID e592e9822ae47a5e236df67dcf296313511f5d37
# Parent  996267ad6fa7c39bc74bf76a36f0f64dc8c69303
tuned tactic

diff -r 996267ad6fa7 -r e592e9822ae4 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 09:21:27 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 09:38:07 2012 +0200
@@ -104,7 +104,7 @@
 
 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
-  subst_tac ctxt NONE [ctor_dtor_corec_like] 1 THEN asm_simp_tac ss_if_True_False 1 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 :: sum_prod_thms_map @ map_ids) THEN
   unfold_thms_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt NONE @{thms unit_eq} THEN' rtac refl) 1);