--- a/src/HOL/Auth/OtwayReesBella.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Auth/OtwayReesBella.thy Thu Apr 18 17:07:01 2013 +0200
@@ -237,10 +237,11 @@
structure OtwayReesBella =
struct
-val analz_image_freshK_ss =
- @{simpset} delsimps [image_insert, image_Un]
+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}
+ addsimps @{thms analz_image_freshK_simps})
end
*}
@@ -251,7 +252,7 @@
(EVERY [REPEAT_FIRST (resolve_tac [allI, ballI, impI]),
REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}),
ALLGOALS (asm_simp_tac
- (Simplifier.context ctxt OtwayReesBella.analz_image_freshK_ss))]))) *}
+ (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))]))) *}
"for proving useful rewrite rule"