src/HOL/Auth/Yahalom.thy

--- a/src/HOL/Auth/Yahalom.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/Auth/Yahalom.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -74,8 +74,7 @@
           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso \<in> yahalom"
 
 
-constdefs 
-  KeyWithNonce :: "[key, nat, event list] => bool"
+definition KeyWithNonce :: "[key, nat, event list] => bool" where
   "KeyWithNonce K NB evs ==
      \<exists>A B na X. 
        Says Server A {|Crypt (shrK A) {|Agent B, Key K, na, Nonce NB|}, X|}