diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/IMPP/Com.thy
--- a/src/HOL/IMPP/Com.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMPP/Com.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -18,10 +18,10 @@
   Arg :: loc and
   Res :: loc
 
-datatype_new vname  = Glb glb | Loc loc
+datatype vname  = Glb glb | Loc loc
 type_synonym globs = "glb => val"
 type_synonym locals = "loc => val"
-datatype_new state  = st globs locals
+datatype state  = st globs locals
 (* for the meta theory, the following would be sufficient:
 typedecl state
 consts   st :: "[globs , locals] => state"
@@ -31,7 +31,7 @@
 
 typedecl pname
 
-datatype_new com
+datatype com
       = SKIP
       | Ass   vname aexp        ("_:==_"                [65, 65    ] 60)
       | Local loc aexp com      ("LOCAL _:=_ IN _"      [65,  0, 61] 60)