diff -r 94b8b70f7bc0 -r e8cf0520c820 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 08:17:43 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:42:07 2010 +0100
@@ -681,7 +681,7 @@
   THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW
-  TRY o (rtac @{thm alpha_gen_compose_sym2} ORELSE' rtac @{thm alpha_gen_compose_sym}) THEN_ALL_NEW
+  TRY o (resolve_tac @{thms alphas_compose_sym2} ORELSE' resolve_tac @{thms alphas_compose_sym}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt)))
 *}
 
@@ -715,7 +715,7 @@
   split_conj_tac THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conj_tac
   THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct)))
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
-  TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW
+  TRY o (eresolve_tac @{thms alphas_compose_trans2} ORELSE' eresolve_tac @{thms alphas_compose_trans}) THEN_ALL_NEW
   (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct)))
 *}
 
@@ -897,7 +897,7 @@
   simp_tac (HOL_basic_ss addsimps @{thms supp_def}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm permute_Abs} :: perm)) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps (@{thm Abs_eq_iff} :: eqiff)) THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps @{thms alphas}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm supp_Pair} :: sym_eqvts ctxt)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps (@{thm Pair_eq} :: all_eqvts ctxt)) THEN_ALL_NEW