diff -r e5ce85418346 -r 4c9f08836d87 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:14:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Wed Apr 24 14:15:01 2013 +0200
@@ -27,8 +27,8 @@
     thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
 
   val mk_map_comp_id_tac: thm -> tactic
-  val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_map_congL_tac: int -> thm -> thm -> tactic
+  val mk_map_cong0_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_map_cong0L_tac: int -> thm -> thm -> tactic
 end;
 
 structure BNF_Tactics : BNF_TACTICS =
@@ -101,12 +101,12 @@
 fun mk_map_comp_id_tac map_comp =
   (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
 
-fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
-  EVERY' [rtac mp, rtac map_cong,
+fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
+  EVERY' [rtac mp, rtac map_cong0,
     CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
 
-fun mk_map_congL_tac passive map_cong map_id' =
-  (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
+fun mk_map_cong0L_tac passive map_cong0 map_id' =
+  (rtac trans THEN' rtac map_cong0 THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   rtac map_id' 1;