src/HOL/Auth/Smartcard/EventSC.thy

--- a/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/Smartcard/EventSC.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -9,10 +9,10 @@
 consts  (*Initial states of agents -- parameter of the construction*)
   initState :: "agent => msg set"
 
-datatype_new card = Card agent
+datatype card = Card agent
 
 text{*Four new events express the traffic between an agent and his card*}
-datatype_new  
+datatype  
   event = Says  agent agent msg
         | Notes agent       msg
         | Gets  agent       msg