--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Thu Aug 29 22:56:39 2013 +0200
@@ -16,7 +16,7 @@
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
+ val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
val mk_kill_bd_card_order_tac: int -> thm -> tactic
@@ -67,21 +67,21 @@
rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
-fun mk_comp_set_map_tac Gmap_comp0 Gmap_cong0 Gset_map set_maps =
+fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
EVERY' ([rtac ext] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
rtac Gmap_cong0] @
- map (fn thm => rtac (thm RS fun_cong)) set_maps @
- [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
+ map (fn thm => rtac (thm RS fun_cong)) set_map0s @
+ [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
- rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
+ rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
- [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
+ [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],