# 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 =