diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Auth/TLS.thy
--- a/src/HOL/Auth/TLS.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/TLS.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -64,10 +64,11 @@
   sessionK :: "(nat*nat*nat) * role => key"
 
 abbreviation
-  clientK :: "nat*nat*nat => key"
+  clientK :: "nat*nat*nat => key" where
   "clientK X == sessionK(X, ClientRole)"
 
-  serverK :: "nat*nat*nat => key"
+abbreviation
+  serverK :: "nat*nat*nat => key" where
   "serverK X == sessionK(X, ServerRole)"