src/ZF/UNITY/Union.thy
changeset 12114 a8e860c86252
parent 11479 697dcaaf478f
child 12195 ed2893765a08
--- 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)