diff -r 1f7cbe39d425 -r 5f79a9e42507 src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Fri Feb 18 16:22:27 2011 +0100
+++ b/src/HOL/Bali/Table.thy	Fri Feb 18 16:36:42 2011 +0100
@@ -29,9 +29,9 @@
 \end{itemize}
 *}
 
-types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
+type_synonym ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
       = "'a \<rightharpoonup> 'b"
-      ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
+type_synonym ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
       = "'a \<Rightarrow> 'b set"