diff -r cf0edebe540c -r ffce25f9aa7f src/HOL/Auth/Yahalom.thy
--- a/src/HOL/Auth/Yahalom.thy	Wed Jan 04 10:28:31 2006 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Wed Jan 04 16:13:53 2006 +0100
@@ -83,7 +83,7 @@
          \<in> set evs"
 
 
-declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare Says_imp_analz_Spy [dest]
 declare parts.Body  [dest]
 declare Fake_parts_insert_in_Un  [dest]
 declare analz_into_parts [dest]
@@ -113,7 +113,8 @@
      "[| Gets B X \<in> set evs; evs \<in> yahalom |]  ==> X \<in> knows Spy evs"
 by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
 
-declare Gets_imp_knows_Spy [THEN analz.Inj, dest]
+lemmas Gets_imp_analz_Spy = Gets_imp_knows_Spy [THEN analz.Inj]
+declare Gets_imp_analz_Spy [dest]
 
 
 text{*Lets us treat YM4 using a similar argument as for the Fake case.*}