--- a/src/HOL/Auth/Public.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Auth/Public.thy Thu Apr 18 17:07:01 2013 +0200
@@ -405,14 +405,16 @@
structure Public =
struct
-val analz_image_freshK_ss = @{simpset} delsimps [image_insert, image_Un]
- delsimps [@{thm imp_disjL}] (*reduces blow-up*)
- addsimps @{thms analz_image_freshK_simps}
+val analz_image_freshK_ss =
+ simpset_of
+ (@{context} delsimps [image_insert, image_Un]
+ delsimps [@{thm imp_disjL}] (*reduces blow-up*)
+ 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 (simpset_of ctxt delsimps [@{thm used_Says}]))
+ (ALLGOALS (simp_tac (ctxt delsimps [@{thm used_Says}]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, @{thm Nonce_supply}]))
@@ -421,7 +423,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]))
@@ -433,7 +435,7 @@
(SIMPLE_METHOD
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}),
- ALLGOALS (asm_simp_tac (Simplifier.context ctxt Public.analz_image_freshK_ss))]))) *}
+ ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))]))) *}
"for proving the Session Key Compromise theorem"