diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -34,10 +34,10 @@
 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*}