--- a/FSet.thy	Wed Nov 04 09:52:31 2009 +0100
+++ b/FSet.thy	Wed Nov 04 10:31:20 2009 +0100
@@ -153,21 +153,16 @@
 term IN
 thm IN_def
 
-(* FIXME: does not work yet 
-quotient_def (for "'a fset")
-  FOLD :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b"
+term fold1
+quotient_def 
+  FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a"
 where
   "FOLD \<equiv> fold1"
-*)
-local_setup {*
-  old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
 
 term fold1
 term fold
 thm fold_def
 
-(* FIXME: does not work yet for all types*)
 quotient_def 
   fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
@@ -177,7 +172,9 @@
 term fmap
 thm fmap_def
 
-ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def fold_def} *}
+ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *}
+ML {* val consts = lookup_quot_consts defs *}
+ML {* val defs_sym = add_lower_defs @{context} defs *}
 
 lemma memb_rsp:
   fixes z