# HG changeset patch
# User traytel
# Date 1392911242 -3600
# Node ID 332641e48ff49d912845c8f407594fda9e9ce362
# Parent  75a639ddc05ff398c89e4d46dc872c118d80ed59# Parent  b1b363e81c87470d01f03c272ba923a2530eba06
merged

diff -r b1b363e81c87 -r 332641e48ff4 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Feb 20 10:32:09 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Feb 20 16:47:22 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