--- a/Nominal/Rsp.thy	Sat Mar 27 08:11:45 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 08:17:43 2010 +0100
@@ -63,7 +63,7 @@
   rel_indtac induct THEN_ALL_NEW
   (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: fvbv_simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)
@@ -83,7 +83,7 @@
    REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
    simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
    asm_full_simp_tac (HOL_ss addsimps (rsp @
-     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
+     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
   ))
 *}
 
@@ -111,7 +111,7 @@
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
-    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alpha_gen}) THEN_ALL_NEW
+    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
   (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
     @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
   THEN_ALL_NEW
@@ -261,7 +261,7 @@
 ML {*
 fun fvbv_rsp_tac' simps ctxt =
   asm_full_simp_tac (HOL_basic_ss addsimps @{thms alpha_gen2}) THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps (@{thm alpha_gen} :: simps)) THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
   REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
   TRY o blast_tac (claset_of ctxt)