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