diff -r 00f8be1b7209 -r f87c8c449018 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Thu Aug 24 00:55:42 2000 +0200
+++ b/src/ZF/Arith.thy	Thu Aug 24 11:05:20 2000 +0200
@@ -56,7 +56,7 @@
   mod  :: [i,i]=>i                    (infixl "mod" 70)
     "m mod n == raw_mod (natify(m), natify(n))"
 
-syntax (symbols)
+syntax (xsymbols)
   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
 
 end