src/HOL/Auth/Public.thy

   addsimps @{thms analz_image_freshK_simps}
 
 (*Tactic for possibility theorems*)
 fun possibility_tac ctxt =
     REPEAT (*omit used_Says so that Nonces start from different traces!*)
-    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}]))
+    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}]))
      THEN
      REPEAT_FIRST (eq_assume_tac ORELSE' 
                    resolve_tac [refl, conjI, @{thm Nonce_supply}]))
 
 (*For harder protocols (such as Recur) where we have to set up some
   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]))
 
 end
 *}