diff -r d67a6a48f1c7 -r 89158f401b07 Nominal/nominal_thmdecls.ML
--- a/Nominal/nominal_thmdecls.ML	Mon Apr 01 23:22:53 2013 +0100
+++ b/Nominal/nominal_thmdecls.ML	Fri Apr 19 00:10:52 2013 +0100
@@ -173,12 +173,12 @@
 (* Transforms a theorem of the form (1) into the form (4). *)
 local
 
-fun tac thm =
+fun tac ctxt thm =
   let
     val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"}
   in
     REPEAT o FIRST'
-      [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms),
+      [CHANGED o simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms),
        rtac (thm RS @{thm "trans"}),
        rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}]
   end
@@ -192,7 +192,7 @@
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c))
     val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt
   in
-    Goal.prove ctxt [] [] goal' (fn _ => tac thm 1)
+    Goal.prove ctxt [] [] goal' (fn {context, ...} => tac context thm 1)
       |> singleton (Proof_Context.export ctxt' ctxt)
       |> (fn th => th RS @{thm "eq_reflection"})
       |> zero_var_indexes
@@ -205,12 +205,13 @@
 (* Transforms a theorem of the form (2) into the form (1). *)
 local
 
-fun tac thm thm' =
+fun tac ctxt thm thm' =
   let
     val ss_thms = @{thms "permute_minus_cancel"(2)}
   in
     EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac,
-      rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (HOL_basic_ss addsimps ss_thms)]
+      rtac @{thm "permute_boolI"}, dtac thm', 
+      full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps ss_thms)]
   end
 
 in
@@ -230,7 +231,7 @@
     val certify = cterm_of (theory_of_thm thm)
     val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm
   in
-    Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1)
+    Goal.prove ctxt' [] [] goal' (fn {context, ...} => tac context thm thm' 1)
       |> singleton (Proof_Context.export ctxt' ctxt)
   end
   handle TERM _ =>