diff -r 25af24e1f37b -r 180f1b3508ed 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