src/HOL/IMP/VCG.thy

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