--- 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;