diff -r 841b7e34e70a -r fe25a3ffeb14 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/nominal_dt_alpha.ML	Tue Jul 27 14:37:59 2010 +0200
@@ -350,7 +350,7 @@
 
   val bound_tac = 
     EVERY' [ rtac exi_zero, 
-             resolve_tac @{thms alpha_gen_refl}, 
+             resolve_tac @{thms alpha_refl}, 
              asm_full_simp_tac (HOL_ss addsimps prod_simps) ]
 in
   REPEAT o FIRST' [rtac @{thm conjI}, 
@@ -407,7 +407,7 @@
 in
   EVERY' 
     [ etac exi_neg,
-      resolve_tac @{thms alpha_gen_sym_eqvt},
+      resolve_tac @{thms alpha_sym_eqvt},
       asm_full_simp_tac (HOL_ss addsimps prod_simps),
       Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
       trans_prem_tac pred_names ctxt ]