--- 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'