src/HOL/Hoare_Parallel/RG_Com.thy

--- a/src/HOL/Hoare_Parallel/RG_Com.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Com.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -12,7 +12,7 @@
 
 type_synonym 'a bexp = "'a set"
 
-datatype 'a com = 
+datatype_new 'a com = 
     Basic "'a \<Rightarrow>'a"
   | Seq "'a com" "'a com"
   | Cond "'a bexp" "'a com" "'a com"