diff -r 7e046ef59fe2 -r bd539b72d484 src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Fri Aug 21 15:56:12 1998 +0200
+++ b/src/HOL/Auth/NS_Shared.thy	Fri Aug 21 16:14:34 1998 +0200
@@ -71,8 +71,7 @@
          (*This message models possible leaks of session keys.
            The two Nonces identify the protocol run: the rule insists upon
            the true senders in order to make them accurate.*)
-    Oops "[| evso: ns_shared;  A ~= Spy;
-             Says B A (Crypt K (Nonce NB)) : set evso;
+    Oops "[| evso: ns_shared;  Says B A (Crypt K (Nonce NB)) : set evso;
              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
                : set evso |]
           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"