--- a/FSet.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/FSet.thy	Mon Nov 02 09:33:48 2009 +0100
@@ -44,7 +44,7 @@
 thm EMPTY_def
 
 quotient_def (for "'a fset")
-  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet"
+  INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 where
   "INSERT \<equiv> op #"
 
@@ -168,10 +168,10 @@
 thm fold_def
 
 (* FIXME: does not work yet for all types*)
-quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+quotient_def (for "'a fset" "'b fset")
+  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fmap \<equiv> map"
 
 term map
 term fmap
@@ -296,6 +296,9 @@
  by simp (rule list_eq_refl)
 
 
+print_quotients
+
+
 ML {* val qty = @{typ "'a fset"} *}
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, quot) = lookup_quot_thms @{context} "fset" *}