1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 19 02:30:45 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 19 03:13:13 2013 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val mk_primcorec_assumption_tac: Proof.context -> tactic
     1.6    val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
     1.7 -  val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
     1.8 +  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> tactic
     1.9    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
    1.10    val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
    1.11      thm list list list -> thm list -> thm list -> thm list -> tactic
    1.12 @@ -74,14 +74,14 @@
    1.13  fun mk_primcorec_sel_of_ctr_tac sel f_ctr =
    1.14    HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel);
    1.15  
    1.16 -fun mk_primcorec_code_of_ctr_case_tac ctxt m f_ctr =
    1.17 +fun mk_primcorec_code_of_ctr_case_tac ctxt f_ctr =
    1.18    HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
    1.19    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.20 -  REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
    1.21 +  REPEAT_DETERM (mk_primcorec_assumption_tac ctxt) THEN
    1.22    HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
    1.23  
    1.24 -fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
    1.25 -  EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);
    1.26 +fun mk_primcorec_code_of_ctr_tac ctxt ctr_thms =
    1.27 +  EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt) ctr_thms);
    1.28  
    1.29  fun mk_primcorec_code_tac ctxt raw collapses =
    1.30    HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN