diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -47,6 +47,8 @@
 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA =
 struct
 
+open Nominal_Permeq
+
 fun lookup xs x = the (AList.lookup (op=) xs x)
 fun group xs = AList.group (op=) xs
 
@@ -505,7 +507,7 @@
       [ etac exi_neg,
         resolve_tac @{thms alpha_sym_eqvt},
         asm_full_simp_tac (HOL_ss addsimps prod_simps),
-        Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+        eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
         trans_prem_tac pred_names ctxt ] 
   end
 
@@ -560,7 +562,7 @@
           resolve_tac @{thms alpha_trans_eqvt}, 
           atac,
           aatac pred_names ctxt, 
-          Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl},
+          eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
           asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
   end