src/HOL/Auth/Recur.thy

--- a/src/HOL/Auth/Recur.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Auth/Recur.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -10,7 +10,7 @@
 
 text{*End marker for message bundles*}
 abbreviation
-  END :: "msg"
+  END :: "msg" where
   "END == Number 0"
 
 (*Two session keys are distributed to each agent except for the initiator,