diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Jul 23 18:44:09 2009 +0200
@@ -204,7 +204,7 @@
     such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
 fun possibility_tac ctxt =
    (REPEAT 
-    (ALLGOALS (simp_tac (local_simpset_of ctxt
+    (ALLGOALS (simp_tac (simpset_of ctxt
           delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] 
           setSolver safe_solver))
      THEN
@@ -215,7 +215,7 @@
   nonces and keys initially*)
 fun basic_possibility_tac ctxt =
     REPEAT 
-    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
+    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
      THEN
      REPEAT_FIRST (resolve_tac [refl, conjI]))