diff -r 5d33c12ccf22 -r d0be2722ce9f src/HOL/Hoare_Parallel/OG_Tran.thy
--- a/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 22:53:18 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tran.thy	Wed Mar 30 23:26:40 2011 +0200
@@ -3,9 +3,8 @@
 
 theory OG_Tran imports OG_Com begin
 
-types
-  'a ann_com_op = "('a ann_com) option"
-  'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
+type_synonym 'a ann_com_op = "('a ann_com) option"
+type_synonym 'a ann_triple_op = "('a ann_com_op \<times> 'a assn)"
   
 primrec com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" where
   "com (c, q) = c"