src/HOL/Auth/TLS.thy

--- a/src/HOL/Auth/TLS.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Auth/TLS.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -49,7 +49,7 @@
 signature.  Therefore, we formalize signature as encryption using the
 private encryption key.*}
 
-datatype_new role = ClientRole | ServerRole
+datatype role = ClientRole | ServerRole
 
 consts
   (*Pseudo-random function of Section 5*)