diff -r 22f8331cdf47 -r d9fc3457554e src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:06:29 1998 +0200
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Sep 15 15:10:38 1998 +0200
@@ -132,7 +132,7 @@
 (** Session keys are not used to encrypt other session keys **)
 
 Goal "evs : yahalom ==>                               \
-\  ALL K KK. KK <= Compl (range shrK) -->                \
+\  ALL K KK. KK <= - (range shrK) -->                 \
 \         (Key K : analz (Key``KK Un (spies evs))) =  \
 \         (K : KK | Key K : analz (spies evs))";
 by (etac yahalom.induct 1);