--- 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),
--- 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),