--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 12:48:20 2014 +0100
@@ -66,7 +66,6 @@
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
- unfold_thms_tac ctxt @{thms split_paired_all} THEN
HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));