# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256913033 -3600
# Node ID 42dac1cfcd14d06d04638fafcec6b38cdd24c9ed
# Parent  22715cab399576b513cfb11b9a8242f1a0b0b192
not sure what changed here

diff -r 22715cab3995 -r 42dac1cfcd14 FSet.thy
--- a/FSet.thy	Fri Oct 30 15:28:44 2009 +0100
+++ b/FSet.thy	Fri Oct 30 15:30:33 2009 +0100
@@ -169,9 +169,9 @@
 
 (* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a 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::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)"
 
 term map
 term fmap