src/HOL/Induct/QuoDataType.thy

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