--- a/FSet.thy	Wed Oct 28 16:16:38 2009 +0100
+++ b/FSet.thy	Wed Oct 28 16:48:57 2009 +0100
@@ -158,16 +158,15 @@
 term fold
 thm fold_def
 
-local_setup {*
-  old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn 
-  @{typ "'a list"} @{typ "'a fset"} #> snd
-*}
+quotient_def (for "'a fset")
+  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+where
+  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
 
 term map
 term fmap
 thm fmap_def
 
-
 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *}
 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *)