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