diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -40,6 +40,8 @@
 structure Nominal_Dt_RawFuns: NOMINAL_DT_RAWFUNS =
 struct
 
+open Nominal_Permeq
+
 (* string list      - type variables of a datatype
    binding          - name of the datatype
    mixfix           - its mixfix
@@ -361,7 +363,7 @@
   SUBPROOF (fn {prems, context, ...} => 
     HEADGOAL 
       (simp_tac (HOL_basic_ss addsimps simps)
-       THEN' Nominal_Permeq.eqvt_tac context [] const_names
+       THEN' eqvt_tac context (eqvt_relaxed_config addexcls const_names)
        THEN' simp_tac (HOL_basic_ss addsimps (prems @ [eqvt_apply_sym]))))
 
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt =