# HG changeset patch
# User traytel
# Date 1407396931 -7200
# Node ID 8e74998e04b803fe6031a1666957de215943033c
# Parent  eea1e7cb4262ce0dac7f4f5225e665197577672e
tuned

diff -r eea1e7cb4262 -r 8e74998e04b8 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Aug 07 10:06:18 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Aug 07 09:35:31 2014 +0200
@@ -973,8 +973,6 @@
                 hyp_subst_tac ctxt,
                 dtac (in_Jrel RS iffD1),
                 dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
-                TRY o
-                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
                 REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_map0s ~~ in_Jrels))])
         (dtor_sets ~~ passive_set_map0s),
diff -r eea1e7cb4262 -r 8e74998e04b8 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Aug 07 10:06:18 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Aug 07 09:35:31 2014 +0200
@@ -682,8 +682,6 @@
                   @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
                 hyp_subst_tac ctxt,
                 dtac (in_Irel RS iffD1), dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
-                TRY o
-                  EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
                 REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
             (rev (active_set_map0s ~~ in_Irels))])
         (ctor_sets ~~ passive_set_map0s),