diff -r d3ad5dc11ab3 -r 7ac5e5c86c7d Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Mon Apr 11 02:25:25 2011 +0100
+++ b/Nominal/nominal_inductive.ML	Wed Apr 13 13:41:52 2011 +0100
@@ -133,8 +133,18 @@
       f x y z u v r s :: map7 f xs ys zs us vs rs ss
 
 (* local abbreviations *)
-fun eqvt_stac ctxt = Nominal_Permeq.eqvt_strict_tac ctxt @{thms permute_minus_cancel} []  
-fun eqvt_srule ctxt = Nominal_Permeq.eqvt_strict_rule ctxt @{thms permute_minus_cancel} []  
+
+local
+  open Nominal_Permeq
+in
+(* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) 
+
+val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel}
+
+fun eqvt_stac ctxt = eqvt_tac ctxt eqvt_sconfig
+fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig  
+
+end
 
 val all_elims = 
   let