diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Induct/QuoDataType.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -10,7 +10,7 @@
 subsection{*Defining the Free Algebra*}
 
 text{*Messages with encryption and decryption as free constructors.*}
-datatype_new
+datatype
      freemsg = NONCE  nat
              | MPAIR  freemsg freemsg
              | CRYPT  nat freemsg