# HG changeset patch
# User desharna
# Date 1418984303 -3600
# Node ID 8713bd81017d6bd49106eb8415b63734fc6dd3d7
# Parent  3f5d6ee7596f153459ea6d8469dfb808e7b9ead9
remove duplication in tactic

diff -r 3f5d6ee7596f -r 8713bd81017d src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Dec 19 11:18:00 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Dec 19 11:18:23 2014 +0100
@@ -468,9 +468,9 @@
     rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
       hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (sels @ rel_injects @ rel_eqs @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
-    ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
-    (rel_injects RL @{thms iffD2[OF eq_True]}) @
-    (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN
+    ((discs @ distincts) RL [eqTrueI, eqFalseI]) @
+    (rel_injects RL [eqTrueI]) @
+    (rel_distincts RL [eqFalseI])) THEN
   TRYALL (resolve_tac [TrueI, refl]);
 
 fun mk_sel_transfer_tac ctxt n sel_defs case_transfer =