diff -r e33b47e4246d -r c0844a30ea4e src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Tue Jan 09 15:22:13 2001 +0100
+++ b/src/HOL/Auth/Public.thy	Tue Jan 09 15:29:17 2001 +0100
@@ -22,11 +22,11 @@
 primrec
         (*Agents know their private key and all public keys*)
   initState_Server  "initState Server     =    
- 		         insert (Key (priK Server)) (Key `` range pubK)"
+ 		         insert (Key (priK Server)) (Key ` range pubK)"
   initState_Friend  "initState (Friend i) =    
- 		         insert (Key (priK (Friend i))) (Key `` range pubK)"
+ 		         insert (Key (priK (Friend i))) (Key ` range pubK)"
   initState_Spy     "initState Spy        =    
- 		         (Key``invKey``pubK``bad) Un (Key `` range pubK)"
+ 		         (Key`invKey`pubK`bad) Un (Key ` range pubK)"
 
 
 rules