--- a/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/SET_Protocol/Event_SET.thy Thu Sep 11 18:54:36 2014 +0200
@@ -15,7 +15,7 @@
text{*Message events*}
-datatype
+datatype_new
event = Says agent agent msg
| Gets agent msg
| Notes agent msg