# HG changeset patch
# User traytel
# Date 1348824711 -7200
# Node ID 204bd497aa4c9680339e765622b910c5dd479cd5
# Parent  e592e9822ae47a5e236df67dcf296313511f5d37
tuned tactic

diff -r e592e9822ae4 -r 204bd497aa4c 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:38:07 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 11:31:51 2012 +0200
@@ -107,7 +107,7 @@
   (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);
+  (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 =>