1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 10:00:07 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Thu Sep 26 10:20:23 2013 +0200
     1.3 @@ -80,6 +80,8 @@
     1.4      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
     1.5    unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
     1.6  
     1.7 +(* TODO: do we need "collapses"? "distincts"? *)
     1.8 +(* TODO: reduce code duplication with selector tactic above *)
     1.9  fun mk_primcorec_code_of_ctr_single_tac ctxt distincts discIs collapses splits split_asms m f_ctr =
    1.10    HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
    1.11    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN