--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 29 22:39:46 2013 +0200
@@ -106,8 +106,8 @@
split_conv}) THEN
rtac refl 1;
-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_comp_id_tac map_comp0 =
+ (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
fun mk_map_cong0_tac m map_cong0 {context = ctxt, prems = _} =
EVERY' [rtac mp, rtac map_cong0,