diff -r 19b47bfac6ef -r 9e7d1c139569 src/HOL/SET_Protocol/Public_SET.thy
--- a/src/HOL/SET_Protocol/Public_SET.thy	Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/SET_Protocol/Public_SET.thy	Thu Apr 18 17:07:01 2013 +0200
@@ -344,7 +344,7 @@
 (*Tactic for possibility theorems*)
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
+    (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]))
@@ -353,7 +353,7 @@
   nonces and keys initially*)
 fun basic_possibility_tac ctxt =
     REPEAT 
-    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
+    (ALLGOALS (asm_simp_tac (ctxt setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac [refl, conjI]))
 *}