src/HOL/Auth/Yahalom2.ML

--- a/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Tue Jan 09 15:29:17 2001 +0100
@@ -149,7 +149,7 @@
 
 Goal "evs : yahalom ==>                               \
 \  ALL K KK. KK <= - (range shrK) -->                 \
-\         (Key K : analz (Key``KK Un (knows Spy evs))) =  \
+\         (Key K : analz (Key`KK Un (knows Spy evs))) =  \
 \         (K : KK | Key K : analz (knows Spy evs))";
 by (etac yahalom.induct 1);
 by analz_knows_Spy_tac;