diff -r 46a14ebdac4f -r a8e860c86252 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Fri Nov 09 00:06:15 2001 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Fri Nov 09 00:09:47 2001 +0100
@@ -38,7 +38,7 @@
    (*standard real numbers as a subset of the hyperreals*)
    SReal_def      "Reals == {x. EX r. x = hypreal_of_real r}"
 
-syntax (symbols)
+syntax (xsymbols)
     approx :: "[hypreal, hypreal] => bool"    (infixl "\\<approx>" 50)
   
 end