diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Auth/Kerberos_BAN.thy
--- a/src/HOL/Auth/Kerberos_BAN.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Kerberos_BAN.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -39,13 +39,15 @@
     by blast
 
 abbreviation
-  CT :: "event list=>nat"
+  CT :: "event list=>nat" where
   "CT == length "
 
-  expiredK :: "[nat, event list] => bool"
+abbreviation
+  expiredK :: "[nat, event list] => bool" where
   "expiredK T evs == sesKlife + T < CT evs"
 
-  expiredA :: "[nat, event list] => bool"
+abbreviation
+  expiredA :: "[nat, event list] => bool" where
   "expiredA T evs == authlife + T < CT evs"