diff -r aa5059a00f41 -r 6fd3fc3254ee Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Wed Sep 21 17:16:11 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Wed Sep 21 10:23:06 2011 +0200
@@ -564,7 +564,7 @@
         [ etac @{thm exE},
           etac @{thm exE},
           perm_inst_tac ctxt, 
-          resolve_tac @{thms alpha_trans_eqvt}, 
+          resolve_tac @{thms alpha_trans_eqvt},
           atac,
           aatac pred_names ctxt, 
           eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},