# HG changeset patch
# User blanchet
# Date 1346852429 -7200
# Node ID a8e74375d971369b4345a50a95967e9bfa3731c8
# Parent  056d6010b6d2caf70f7a2645b6cf727192ed60a3
fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors

diff -r 056d6010b6d2 -r a8e74375d971 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 15:40:28 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Wed Sep 05 15:40:29 2012 +0200
@@ -195,7 +195,7 @@
                 (Drule.instantiate' (map (SOME o certifyT lthy) prod_Ts) [] (mk_sumEN n))
               |> Morphism.thm phi;
           in
-            mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf_thm sumEN_thm'
+            mk_exhaust_tac ctxt n ctr_defs fld_iff_unf_thm sumEN_thm'
           end;
 
         val inject_tacss =
diff -r 056d6010b6d2 -r a8e74375d971 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 05 15:40:28 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 05 15:40:29 2012 +0200
@@ -8,7 +8,7 @@
 signature BNF_FP_SUGAR_TACTICS =
 sig
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
-  val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
+  val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
@@ -27,12 +27,11 @@
    REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
    rtac refl) 1;
 
-fun mk_exhaust_tac ctxt n ms ctr_defs fld_iff_unf sumEN' =
+fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
   Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
   Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
-  EVERY' (map2 (fn k => fn m =>
-    select_prem_tac n (rotate_tac 1) k THEN' REPEAT_DETERM_N m o dtac @{thm meta_spec} THEN'
-    etac @{thm meta_mp} THEN' atac) (1 upto n) ms) 1;
+  EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
+    etac @{thm meta_mp}, atac]) (1 upto n)) 1;
 
 fun mk_fld_iff_unf_tac ctxt cTs cfld cunf fld_unf unf_fld =
   (rtac iffI THEN'