--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 16:46:53 2013 +0200
@@ -217,13 +217,13 @@
val n = length set_map's;
in
REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
- unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
+ unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
- rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+ rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
- etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]}))
+ etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
set_map's,
rtac conjI,
EVERY' (map (fn convol =>