src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49684 1cf810b8f600
parent 49585 5c4a12550491
child 50058 bb1fadeba35e
--- 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,