--- 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*}