diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -35,10 +35,10 @@
 definition symKeys :: "key set" where
   "symKeys == {K. invKey K = K}"
 
-datatype  --{*We allow any number of friendly agents*}
+datatype_new  --{*We allow any number of friendly agents*}
   agent = Server | Friend nat | Spy
 
-datatype
+datatype_new
      msg = Agent  agent     --{*Agent names*}
          | Number nat       --{*Ordinary integers, timestamps, ...*}
          | Nonce  nat       --{*Unguessable nonces*}