--- a/src/HOL/NanoJava/Decl.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/NanoJava/Decl.thy Thu Sep 11 19:32:36 2014 +0200
@@ -7,7 +7,7 @@
theory Decl imports Term begin
-datatype_new ty
+datatype ty
= NT --{* null type *}
| Class cname --{* class type *}