--- a/src/HOL/Bali/Table.thy Sat Jan 14 16:12:09 2012 +0100
+++ b/src/HOL/Bali/Table.thy Sat Jan 14 16:14:22 2012 +0100
@@ -280,9 +280,8 @@
done
-definition
- Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
- where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
+definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
+ where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)"
definition
overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100)