src/HOL/Auth/Event.thy

--- a/src/HOL/Auth/Event.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Event.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -15,7 +15,7 @@
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
 
-datatype_new
+datatype
   event = Says  agent agent msg
         | Gets  agent       msg
         | Notes agent       msg