--- a/Nominal/nominal_eqvt.ML	Mon Apr 01 23:22:53 2013 +0100
+++ b/Nominal/nominal_eqvt.ML	Fri Apr 19 00:10:52 2013 +0100
@@ -18,14 +18,14 @@
 open Nominal_Permeq;
 open Nominal_ThmDecls;
 
-val atomize_conv =
+fun atomize_conv ctxt =
   Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE))
-    (HOL_basic_ss addsimps @{thms induct_atomize})
+    (put_simpset HOL_basic_ss ctxt addsimps @{thms induct_atomize})
 
-val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv)
+fun atomize_intr ctxt = Conv.fconv_rule (Conv.prems_conv ~1 (atomize_conv ctxt))
 
 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
-  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt))
+  (Conv.params_conv ~1 (K (Conv.prems_conv ~1 (atomize_conv ctxt))) ctxt))
 
 
 (** equivariance tactics **)
@@ -36,8 +36,10 @@
     val cpi = Thm.cterm_of thy pi
     val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI}
     val eqvt_sconfig = eqvt_strict_config addexcls pred_names
-    val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all}
-    val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)}
+    val simps1 = 
+      put_simpset HOL_basic_ss ctxt addsimps @{thms permute_fun_def permute_self split_paired_all}
+    val simps2 = 
+      put_simpset HOL_basic_ss ctxt addsimps @{thms permute_bool_def permute_minus_cancel(2)}
   in
     eqvt_tac ctxt eqvt_sconfig THEN'
     SUBPROOF (fn {prems, context as ctxt, ...} =>
@@ -86,7 +88,7 @@
 
     val pred_names = map (name_of o head_of) preds
     val raw_induct' = atomize_induct ctxt raw_induct
-    val intrs' = map atomize_intr intrs
+    val intrs' = map (atomize_intr ctxt) intrs
 
     val (([raw_concl], [raw_pi]), ctxt') =
       ctxt