--- a/src/HOL/Bali/Type.thy Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Bali/Type.thy Tue Sep 09 20:51:36 2014 +0200
@@ -14,13 +14,13 @@
\end{itemize}
*}
-datatype prim_ty --{* primitive type, cf. 4.2 *}
+datatype_new prim_ty --{* primitive type, cf. 4.2 *}
= Void --{* result type of void methods *}
| Boolean
| Integer
-datatype ref_ty --{* reference type, cf. 4.3 *}
+datatype_new ref_ty --{* reference type, cf. 4.3 *}
= NullT --{* null type, cf. 4.1 *}
| IfaceT qtname --{* interface type *}
| ClassT qtname --{* class type *}