tuning

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

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 15:33:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 15:33:32 2013 +0200
@@ -10,9 +10,9 @@
   val mk_primcorec_taut_tac: Proof.context -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
-  val mk_primcorec_dtr_to_ctr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
-  val mk_primcorec_eq_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
-    thm list -> thm list -> thm list -> tactic
+  val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
+  val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
+    thm list list list -> thm list -> thm list -> thm list -> tactic
   val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
 end;
 
@@ -54,12 +54,12 @@
 fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
   mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_eq_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
+fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
   mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
   unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
     maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
 
-fun mk_primcorec_dtr_to_ctr_tac ctxt m collapse disc sels =
+fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels =
   HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
 

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