src/HOL/Auth/Yahalom2.thy

--- a/src/HOL/Auth/Yahalom2.thy	Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.thy	Fri Aug 21 16:14:34 1998 +0200
@@ -64,7 +64,7 @@
          (*This message models possible leaks of session keys.  The nonces
            identify the protocol run.  Quoting Server here ensures they are
            correct. *)
-    Oops "[| evso: yahalom;  A ~= Spy;
+    Oops "[| evso: yahalom;  
              Says Server A {|Nonce NB, 
                              Crypt (shrK A) {|Agent B, Key K, Nonce NA|},
                              X|}  : set evso |]