src/HOL/Auth/Message.thy

       is the private key and vice versa*}
 
 definition symKeys :: "key set" where
   "symKeys == {K. invKey K = K}"
 
-datatype_new  --{*We allow any number of friendly agents*}
+datatype  --{*We allow any number of friendly agents*}
   agent = Server | Friend nat | Spy
 
-datatype_new
+datatype
      msg = Agent  agent     --{*Agent names*}
          | Number nat       --{*Ordinary integers, timestamps, ...*}
          | Nonce  nat       --{*Unguessable nonces*}
          | Key    key       --{*Crypto keys*}
          | Hash   msg       --{*Hashing*}