diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_quot.ML
--- a/Nominal/nominal_dt_quot.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_quot.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -49,6 +49,8 @@
 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT =
 struct
 
+open Nominal_Permeq
+
 fun lookup xs x = the (AList.lookup (op=) xs x)
 
 
@@ -172,7 +174,7 @@
     val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair}
   in
     EVERY' [ simp_tac ss1,
-             Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [],
+             eqvt_tac ctxt (eqvt_strict_config addpres perm_simps),
              simp_tac ss2 ]
   end
 
@@ -299,11 +301,12 @@
             case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of
               SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses)
             | NONE => mk_bn_supp_abs_tac fv_fun
+          val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts)
         in
           EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)),
                    TRY o supp_abs_tac,
                    TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}),
-                   TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], 
+                   TRY o eqvt_tac ctxt eqvt_rconfig, 
                    TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)),
                    TRY o asm_full_simp_tac (add_ss thms3),
                    TRY o simp_tac (add_ss thms2),
@@ -373,7 +376,7 @@
     val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs
     val ss_tac = 
       EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss),
-              TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [],
+              TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts),
               TRY o asm_full_simp_tac HOL_basic_ss]
   in
     induct_prove qtys props qinduct (K ss_tac) ctxt'
@@ -519,8 +522,8 @@
      in
        [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2)))
          |> (if rec_flag
-             then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []
-             else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ]
+             then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)
+             else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ]
      end
 
 
@@ -556,8 +559,8 @@
             val (abs_eqs, peqs) = split_filter is_abs_eq eqs
 
             val fprops' = 
-              map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops
-              @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops
+              map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops
+              @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops
 
             (* for freshness conditions *) 
             val tac1 = SOLVED' (EVERY'