--- a/src/HOL/Bali/Table.thy Mon Mar 01 12:30:55 2010 +0100
+++ b/src/HOL/Bali/Table.thy Mon Mar 01 13:42:31 2010 +0100
@@ -51,9 +51,7 @@
by (simp add: map_add_def)
section {* Conditional Override *}
-constdefs
-cond_override::
- "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
+definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
--{* when merging tables old and new, only override an entry of table old when
the condition cond holds *}
@@ -98,8 +96,7 @@
section {* Filter on Tables *}
-constdefs
-filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
+definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
"filter_tab c t \<equiv> \<lambda> k. (case t k of
None \<Rightarrow> None
| Some x \<Rightarrow> if c k x then Some x else None)"