--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Wed Feb 17 21:51:56 2016 +0100
@@ -809,9 +809,9 @@
(*Because initState contains a set of nonces, this is needed for base case of
analz_image_freshK*)
-lemma analz_image_Key_Un_Nonce: "analz (Key`K \<union> Nonce`N) = Key`K \<union> Nonce`N"
-apply auto
-done
+lemma analz_image_Key_Un_Nonce:
+ "analz (Key ` K \<union> Nonce ` N) = Key ` K \<union> Nonce ` N"
+ by (auto simp del: parts_image)
method_setup sc_analz_freshK = \<open>
Scan.succeed (fn ctxt =>