src/HOL/Auth/TLS.thy

--- a/src/HOL/Auth/TLS.thy	Wed Jun 24 10:29:46 1998 +0200
+++ b/src/HOL/Auth/TLS.thy	Wed Jun 24 10:30:29 1998 +0200
@@ -61,8 +61,8 @@
     clientK, serverK :: "nat*nat*nat => key"
 
 translations
-  "clientK (nonces)"	== "sessionK(nonces,0)"
-  "serverK (nonces)"	== "sessionK(nonces,1)"
+  "clientK X" == "sessionK(X,0)"
+  "serverK X" == "sessionK(X,1)"
 
 rules
   (*the pseudo-random function is collision-free*)