# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271845552 -7200
# Node ID a0c7290a4e2770b4c089902cadbdf75c6a836c05
# Parent  c8b31085cb5b59467085d1e511a4a10fa734cb39
infix for In

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"