--- a/Nominal/nominal_inductive.ML	Thu Apr 28 11:44:36 2011 +0800
+++ b/Nominal/nominal_inductive.ML	Thu Apr 28 11:51:01 2011 +0800
@@ -139,10 +139,10 @@
 in
 (* by default eqvt_strict_config contains unwanted @{thm permute_pure} *) 
 
-val eqvt_sconfig = (delposts eqvt_strict_config) addpres @{thms permute_minus_cancel}
+val eqvt_sconfig = 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  
+fun eqvt_srule ctxt = eqvt_rule ctxt eqvt_sconfig
 
 end
 
@@ -175,7 +175,9 @@
       val prm_tys = map (fastype_of o term_of) prms
       val cperms = map (cterm_of thy o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
-      val prem' = cterm_instantiate (intr_cvars ~~ p_prms) prem
+      val prem' = prem
+        |> cterm_instantiate (intr_cvars ~~ p_prms) 
+        |> eqvt_srule ctxt
 
       (* for inductive-premises*)
       fun tac1 prm = helper_tac true prm p context 
@@ -189,7 +191,9 @@
       fun select prm (t, i) =
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
     in
-      EVERY1 [eqvt_stac ctxt, rtac prem', RANGE (map (SUBGOAL o select) prems) ]
+      EVERY1 [ eqvt_stac context, 
+               rtac prem', 
+               RANGE (map (SUBGOAL o select) prems) ]
     end) ctxt
 
 fun fresh_thm ctxt user_thm p c concl_args avoid_trm =
@@ -244,7 +248,9 @@
 
       val cperms = map (cterm_of thy o perm_const) prm_tys
       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 
-      val prem' = cterm_instantiate (intr_cvars ~~ qp_prms) prem
+      val prem' = prem
+        |> cterm_instantiate (intr_cvars ~~ qp_prms)
+        |> eqvt_srule ctxt
 
       val fprop' = eqvt_srule ctxt' fprop 
       val tac_fresh = simp_tac (HOL_basic_ss addsimps [fprop'])
@@ -277,7 +283,8 @@
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
     val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
-    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ]
+    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, 
+             if null avoid then tac1 else tac2 ]
   end
 
 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args