--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 18:31:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 18:44:03 2013 +0200
@@ -13,7 +13,7 @@
val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
- val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
+ val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
@@ -58,9 +58,9 @@
unfold_thms_tac ctxt [collect_set_map RS sym] THEN
rtac refl 1;
-fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
+fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
- map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
+ map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong0 map_comps =
EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,