diff -r 69917bbbce45 -r 89f162de39cf src/HOL/Auth/Shared.thy
--- a/src/HOL/Auth/Shared.thy	Fri Jul 24 13:02:01 1998 +0200
+++ b/src/HOL/Auth/Shared.thy	Fri Jul 24 13:03:20 1998 +0200
@@ -17,7 +17,7 @@
   isSym_keys "isSymKey K"	(*All keys are symmetric*)
   inj_shrK   "inj shrK"		(*No two agents have the same long-term key*)
 
-primrec initState agent
+primrec
         (*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))}"