diff -r 46a14ebdac4f -r a8e860c86252 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Fri Nov 09 00:06:15 2001 +0100
+++ b/src/ZF/UNITY/Union.thy	Fri Nov 09 00:09:47 2001 +0100
@@ -50,7 +50,7 @@
   "JN x y. B"   == "JN x. JN y. B"
   "JN x. B"     == "JOIN(state,(%x. B))"
 
-syntax (symbols)
+syntax (xsymbols)
    SKIP     :: i                    ("\\<bottom>")
   "op Join" :: [i, i] => i   (infixl "\\<squnion>" 65)
   "@JOIN1"  :: [pttrns, i] => i     ("(3\\<Squnion> _./ _)" 10)