1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 15:33:31 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 15:33:32 2013 +0200
     1.3 @@ -772,7 +772,7 @@
     1.4                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
     1.5                |> curry Logic.list_all (map dest_Free (#fun_args sel_eqn));
     1.6            in
     1.7 -            mk_primcorec_eq_tac lthy def_thms sel_corec k m exclsss
     1.8 +            mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss
     1.9                nested_maps nested_map_idents nested_map_comps
    1.10              |> K |> Goal.prove lthy [] [] t
    1.11            end;

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 15:33:31 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 15:33:32 2013 +0200
     2.3 @@ -10,9 +10,9 @@
     2.4    val mk_primcorec_taut_tac: Proof.context -> tactic
     2.5    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     2.6      tactic
     2.7 -  val mk_primcorec_dtr_to_ctr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
     2.8 -  val mk_primcorec_eq_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     2.9 -    thm list -> thm list -> thm list -> tactic
    2.10 +  val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
    2.11 +  val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
    2.12 +    thm list list list -> thm list -> thm list -> thm list -> tactic
    2.13    val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
    2.14  end;
    2.15  
    2.16 @@ -54,12 +54,12 @@
    2.17  fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
    2.18    mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
    2.19  
    2.20 -fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
    2.21 +fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
    2.22    mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
    2.23    unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
    2.24      maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
    2.25  
    2.26 -fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
    2.27 +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels =
    2.28    HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
    2.29    unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
    2.30  

     3.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Sep 18 15:33:31 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Sep 18 15:33:32 2013 +0200
     3.3 @@ -51,7 +51,8 @@
     3.4      rtac (Drule.instantiate_normalize insts thm) 1
     3.5    end);
     3.6  
     3.7 -fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
     3.8 +fun unfold_thms_tac _ [] = all_tac
     3.9 +  | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
    3.10  
    3.11  fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
    3.12