diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/Hoare_Parallel/OG_Com.thy
--- a/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Com.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -14,7 +14,7 @@
 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a
 com"} for non-annotated commands. *}
 
-datatype_new 'a ann_com = 
+datatype 'a ann_com = 
      AnnBasic "('a assn)"  "('a \<Rightarrow> 'a)"         
    | AnnSeq "('a ann_com)"  "('a ann_com)"   
    | AnnCond1 "('a assn)"  "('a bexp)"  "('a ann_com)"  "('a ann_com)"