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