--- a/src/HOL/Auth/OtwayRees_Bad.ML Thu Feb 05 10:26:59 1998 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Thu Feb 05 10:38:34 1998 +0100
@@ -266,8 +266,8 @@
(*Only it is FALSE. Somebody could make a fake message to Server
substituting some other nonce NA' for NB.*)
goal thy
- "!!evs. [| A ~: bad; A ~= Spy; evs : otway |] \
-\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
+ "!!evs. [| A ~: bad; evs : otway |] \
+\ ==> Crypt (shrK A) {|NA, Key K|} : parts (spies evs) --> \
\ Says A B {|NA, Agent A, Agent B, \
\ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \
\ : set evs --> \