diff -r 09dff5ef8f74 -r f0a78fda343f Quot/Examples/FSet3.thy
--- a/Quot/Examples/FSet3.thy	Sat Dec 26 20:24:53 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Sat Dec 26 20:45:37 2009 +0100
@@ -519,10 +519,6 @@
   as "delete_raw"
 
 quotient_definition
-  "funion :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<union>f _" [50, 51] 50)
-  as "op @"
-
-quotient_definition
   "finter :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" ("_ \<inter>f _" [70, 71] 70)
   as "inter_raw"