# HG changeset patch
# User blanchet
# Date 1346836098 -7200
# Node ID 93f281430e7745ee3529a957cbd737fe509da24e
# Parent  0da8120bd2aa6b2f10c21ea109f68ea9d8fb8270
fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case

diff -r 0da8120bd2aa -r 93f281430e77 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:08:18 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:08:18 2012 +0200
@@ -315,7 +315,7 @@
                 nth exist_xs_v_eq_ctrs (k - 1));
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_alternate_disc_def_tac ctxt (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
+              mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
                 exhaust_thm')
             |> singleton (Proof_Context.export names_lthy lthy)
             |> Thm.close_derivation
diff -r 0da8120bd2aa -r 93f281430e77 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:08:18 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:08:18 2012 +0200
@@ -7,7 +7,7 @@
 
 signature BNF_WRAP_TACTICS =
 sig
-  val mk_alternate_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic
+  val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
   val mk_case_cong_tac: thm -> thm list -> tactic
   val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
@@ -41,10 +41,11 @@
 fun mk_unique_disc_def_tac m exhaust' =
   EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
 
-fun mk_alternate_disc_def_tac ctxt other_disc_def distinct exhaust' =
-  EVERY' [subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
+fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
+  EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
     SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
-    rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1;
+    rtac exhaust'] @
+    (([etac notE, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1;
 
 fun mk_half_disc_exclude_tac m discD disc'_thm =
   (dtac discD THEN'