src/HOL/IMP/VCG.thy

--- a/src/HOL/IMP/VCG.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/IMP/VCG.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -7,7 +7,7 @@
 text{* Annotated commands: commands where loops are annotated with
 invariants. *}
 
-datatype_new acom =
+datatype acom =
   Askip                  ("SKIP") |
   Aassign vname aexp     ("(_ ::= _)" [1000, 61] 61) |
   Aseq   acom acom       ("_;;/ _"  [60, 61] 60) |