diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/MicroJava/J/Example.thy
--- a/src/HOL/MicroJava/J/Example.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/MicroJava/J/Example.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -36,8 +36,8 @@
 \end{verbatim}
 *}
 
-datatype_new cnam' = Base' | Ext'
-datatype_new vnam' = vee' | x' | e'
+datatype cnam' = Base' | Ext'
+datatype vnam' = vee' | x' | e'
 
 text {*
   @{text cnam'} and @{text vnam'} are intended to be isomorphic