src/HOL/IMP/ACom.thy
changeset 58249 180f1b3508ed
parent 57512 cc97b347b301
child 58310 91ea607a34d8
--- a/src/HOL/IMP/ACom.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/IMP/ACom.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -6,7 +6,7 @@
 
 subsection "Annotated Commands"
 
-datatype 'a acom =
+datatype_new 'a acom =
   SKIP 'a                           ("SKIP {_}" 61) |
   Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |