diff -r 597efdb7decb -r aafe719dff14 src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Wed Sep 17 16:40:52 1997 +0200
+++ b/src/HOL/Auth/Shared.thy	Thu Sep 18 13:24:04 1997 +0200
@@ -21,7 +21,7 @@
         (*Server knows all long-term keys; other agents know only their own*)
   initState_Server  "initState Server     = Key `` range shrK"
   initState_Friend  "initState (Friend i) = {Key (shrK (Friend i))}"
-  initState_Spy     "initState Spy        = Key``shrK``lost"
+  initState_Spy     "initState Spy        = Key``shrK``bad"
 
 
 rules