src/HOL/Bali/Type.thy
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58887 38db8ddc0f57
--- a/src/HOL/Bali/Type.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Bali/Type.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -14,13 +14,13 @@
 \end{itemize}
 *}
 
-datatype_new prim_ty        --{* primitive type, cf. 4.2 *}
+datatype prim_ty        --{* primitive type, cf. 4.2 *}
         = Void          --{* result type of void methods *}
         | Boolean
         | Integer
 
 
-datatype_new ref_ty         --{* reference type, cf. 4.3 *}
+datatype ref_ty         --{* reference type, cf. 4.3 *}
         = NullT         --{* null type, cf. 4.1 *}
         | IfaceT qtname --{* interface type *}
         | ClassT qtname --{* class type *}