src/HOL/MicroJava/J/Example.thy

--- a/src/HOL/MicroJava/J/Example.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -36,8 +36,8 @@
 \end{verbatim}
 *}
 
-datatype cnam' = Base' | Ext'
-datatype vnam' = vee' | x' | e'
+datatype_new cnam' = Base' | Ext'
+datatype_new vnam' = vee' | x' | e'
 
 text {*
   @{text cnam'} and @{text vnam'} are intended to be isomorphic