1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 15:13:28 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 15:13:55 2013 +0200
     1.3 @@ -9,8 +9,8 @@
     1.4  sig
     1.5    val mk_primcorec_assumption_tac: Proof.context -> thm list -> tactic
     1.6    val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
     1.7 -    thm list -> int list -> thm list -> tactic
     1.8 -  val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> thm list -> tactic
     1.9 +    int list -> thm list -> tactic
    1.10 +  val mk_primcorec_code_of_raw_tac: thm list -> thm list -> thm -> tactic
    1.11    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
    1.12    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    1.13      tactic
    1.14 @@ -83,33 +83,31 @@
    1.15      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    1.16    unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
    1.17  
    1.18 -(* TODO: do we need "collapses"? *)
    1.19  (* TODO: reduce code duplication with selector tactic above *)
    1.20 -fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
    1.21 +fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
    1.22    HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
    1.23    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    1.24    REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt discIs) THEN
    1.25    HEADGOAL (SELECT_GOAL (HEADGOAL (REPEAT_DETERM o
    1.26      (rtac refl ORELSE' atac ORELSE'
    1.27 -     eresolve_tac (falseEs @ map (fn thm => thm RS trans) collapses) ORELSE'
    1.28       resolve_tac split_connectI ORELSE'
    1.29       Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.30       Splitter.split_tac (split_if :: splits) ORELSE'
    1.31       eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    1.32       (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac))));
    1.33  
    1.34 -fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs collapses splits split_asms ms ctr_thms =
    1.35 -  EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits
    1.36 -    split_asms) ms ctr_thms);
    1.37 +fun mk_primcorec_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
    1.38 +  EVERY (map2 (mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
    1.39 +    ms ctr_thms);
    1.40  
    1.41 -fun mk_primcorec_code_of_raw_tac splits disc_excludes raw collapses =
    1.42 +fun mk_primcorec_code_of_raw_tac splits disc_excludes raw =
    1.43    HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
    1.44      (rtac refl ORELSE'
    1.45       (TRY o rtac sym) THEN' atac ORELSE'
    1.46       resolve_tac split_connectI ORELSE'
    1.47       Splitter.split_tac (split_if :: splits) ORELSE'
    1.48       etac notE THEN' atac ORELSE'
    1.49 -     dresolve_tac disc_excludes THEN' etac notE THEN' atac ORELSE'
    1.50 -     eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
    1.51 +     (TRY o dresolve_tac disc_excludes) THEN' etac notE THEN' atac));
    1.52 +
    1.53  
    1.54  end;