--- 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]))