# HG changeset patch
# User traytel
# Date 1349162428 -7200
# Node ID 1cf810b8f6004317f518dd67d08ee0c7003bb0c4
# Parent  78a3d5006cf13efd6d08326fce03c4fc2a3c7e10
made tactic more robust (less usage of stac)

diff -r 78a3d5006cf1 -r 1cf810b8f600 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Oct 02 01:00:18 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Oct 02 09:20:28 2012 +0200
@@ -288,12 +288,12 @@
         REPEAT_DETERM o etac conjE,
         hyp_subst_tac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE],
-        rtac bexI, rtac conjI, rtac trans, rtac map_comp,
-        REPEAT_DETERM_N m o stac @{thm id_o},
-        REPEAT_DETERM_N n o stac @{thm o_id},
-        etac sym, rtac trans, rtac map_comp,
-        REPEAT_DETERM_N m o stac @{thm id_o},
-        REPEAT_DETERM_N n o stac @{thm o_id},
+        rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
+        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
+        etac sym, rtac trans, rtac map_comp, rtac trans, rtac map_cong,
+        REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
+        REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
         rtac trans, rtac map_cong,
         REPEAT_DETERM_N m o EVERY' [rtac @{thm diagE'}, etac set_mp, atac],
         REPEAT_DETERM_N n o rtac refl,