1.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:18:48 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Wed Sep 05 11:37:22 2012 +0200
     1.3 @@ -424,7 +424,7 @@
     1.4              val goal = mk_Trueprop_eq (caseB_fs $ v, mk_rhs discs fs selss);
     1.5            in
     1.6              Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
     1.7 -              mk_case_eq_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
     1.8 +              mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
     1.9              |> singleton (Proof_Context.export names_lthy lthy)
    1.10            end;
    1.11  

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:18:48 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Wed Sep 05 11:37:22 2012 +0200
     2.3 @@ -9,7 +9,8 @@
     2.4  sig
     2.5    val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
     2.6    val mk_case_cong_tac: thm -> thm list -> tactic
     2.7 -  val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
     2.8 +  val mk_case_eq_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list ->
     2.9 +    tactic
    2.10    val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    2.11    val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    2.12    val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
    2.13 @@ -29,8 +30,10 @@
    2.14  fun triangle _ [] = []
    2.15    | triangle k (xs :: xss) = take k xs :: triangle (k + 1) xss
    2.16  
    2.17 -fun mk_if_P_or_not_P thm =
    2.18 -  thm RS @{thm if_not_P} handle THM _ => thm RS @{thm if_P}
    2.19 +fun mk_case_if_P_or_not_Ps n k thms =
    2.20 +  let val (negs, pos) = split_last thms in
    2.21 +    map (fn thm => thm RS @{thm if_not_P}) negs @ (if k = n then [] else [pos RS @{thm if_P}])
    2.22 +  end;
    2.23  
    2.24  fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
    2.25  
    2.26 @@ -71,13 +74,12 @@
    2.27        SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
    2.28        rtac refl)) 1;
    2.29  
    2.30 -fun mk_case_eq_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
    2.31 +fun mk_case_eq_tac ctxt n exhaust' case_thms disc_thmss' sel_thmss =
    2.32    (rtac exhaust' THEN'
    2.33     EVERY' (map3 (fn case_thm => fn if_disc_thms => fn sel_thms =>
    2.34 -       EVERY' [hyp_subst_tac THEN'
    2.35 -         SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)) THEN' rtac case_thm])
    2.36 -     case_thms (map (map mk_if_P_or_not_P) (triangle 1 (map (fst o split_last) disc_thmss')))
    2.37 -     sel_thmss)) 1;
    2.38 +       EVERY' [hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt (if_disc_thms @ sel_thms)),
    2.39 +         rtac case_thm])
    2.40 +     case_thms (map2 (mk_case_if_P_or_not_Ps n) (1 upto n) (triangle 1 disc_thmss')) sel_thmss)) 1;
    2.41  
    2.42  fun mk_case_cong_tac exhaust' case_thms =
    2.43    (rtac exhaust' THEN'