# HG changeset patch
# User blanchet
# Date 1393847300 -3600
# Node ID 75907f171d4ce5b0af13314b0d9c685965ce4909
# Parent  a28817253b31659e19d1313836771a7a22b72ada
removed obsolete, harmful step in tactic

diff -r a28817253b31 -r 75907f171d4c src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- 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)));