diff -r c8b31085cb5b -r a0c7290a4e27 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Wed Apr 21 10:24:39 2010 +0200
+++ b/Nominal/FSet.thy	Wed Apr 21 12:25:52 2010 +0200
@@ -370,7 +370,7 @@
   "{|x|}"     == "CONST finsert x {||}"
 
 quotient_definition
-  fin ("_ |\<in>| _" [50, 51] 50)
+  fin (infix "|\<in>|" 50)
 where
   "fin :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" is "memb"