src/HOL/Auth/TLS.ML

--- a/src/HOL/Auth/TLS.ML	Mon Mar 08 13:49:53 1999 +0100
+++ b/src/HOL/Auth/TLS.ML	Tue Mar 09 11:01:39 1999 +0100
@@ -480,7 +480,7 @@
 (*ClientAccepts and ServerAccepts: because PMS was already visible*)
 by (REPEAT (blast_tac (claset() addDs [Spy_not_see_PMS, 
 				       Says_imp_spies RS analz.Inj,
-				       Notes_imp_spies RS analz.Inj]) 6));
+				       Notes_imp_knows_Spy RS analz.Inj]) 6));
 (*ClientHello*)
 by (Blast_tac 3);
 (*SpyKeys: by secrecy of the PMS, Spy cannot make the MS*)