diff -r 1810b1ade437 -r 47ee18b6ae32 src/HOL/Bali/Table.thy
--- 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)"