diff -r 6a114f8d45e6 -r 94b8b70f7bc0 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Sat Mar 27 08:11:45 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 08:17:43 2010 +0100
@@ -653,7 +653,7 @@
   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
   THEN_ALL_NEW split_conj_tac THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv
        add_0_left supp_zero_perm Int_empty_left split_conv})
 *}
 
@@ -898,7 +898,7 @@
   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 alpha_gen}) 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
   simp_tac (HOL_basic_ss addsimps @{thms supp_at_base[symmetric,simplified supp_def]}) THEN_ALL_NEW