--- a/src/HOL/Auth/Guard/GuardK.thy Tue Aug 16 19:25:32 2005 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy Tue Aug 16 19:25:42 2005 +0200
@@ -270,7 +270,7 @@
apply (clarsimp, blast)
(* K ~:invKey`Ks *)
apply (subgoal_tac "GuardK n Ks (set (decrypt' l' K Y))")
-apply (drule_tac x="decrypt' l' K Y" in spec, simp add: set_mem_eq)
+apply (drule_tac x="decrypt' l' K Y" in spec, simp add: mem_iff)
apply (subgoal_tac "Crypt K Y:parts (set l)")
apply (drule parts_cnb, rotate_tac -1, simp)
apply (clarify, drule_tac X="Key Ka" and H="insert Y (set l')" in analz_sub)