# HG changeset patch
# User traytel
# Date 1392907886 -3600
# Node ID 75a639ddc05ff398c89e4d46dc872c118d80ed59
# Parent  42e4e8c2e8dcf02bc4815d8c0fc7cf05f84900b9
tuned tactic

diff -r 42e4e8c2e8dc -r 75a639ddc05f src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Feb 20 15:14:37 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Feb 20 15:51:26 2014 +0100
@@ -427,16 +427,16 @@
       CONJ_WRAP' (fn rv_Cons =>
         CONJ_WRAP' (fn (i, rv_Nil) => (EVERY' [rtac exI,
           rtac (@{thm append_Nil} RS arg_cong RS trans),
-          rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS arg_cong RS trans), rtac rv_Nil]))
+          rtac (rv_Cons RS trans), rtac (mk_sum_caseN n i RS trans), rtac rv_Nil]))
         (ks ~~ rv_Nils))
       rv_Conss,
       REPEAT_DETERM o rtac allI, rtac (mk_sumEN n),
       EVERY' (map (fn i =>
         CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
           CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
-            rtac (@{thm append_Cons} RS arg_cong RS trans),
-            rtac (rv_Cons RS trans), etac (sum_weak_case_cong RS arg_cong RS trans),
-            rtac (mk_sum_caseN n i RS arg_cong RS trans), atac])
+            rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
+            if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
+            rtac (mk_sum_caseN n i RS trans), atac])
           ks])
         rv_Conss)
       ks)] 1