diff -r b36874cf3b0b -r e540b7d4ecb1 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Feb 03 13:59:00 1994 +0100
@@ -271,7 +271,7 @@
 
 
 fun syntax_error toks =
-  error ("Syntax error at: " ^ space_implode " " (map str_of_token toks));
+  error ("Syntax error at: " ^ quote (space_implode " " (map str_of_token toks)));
 
 fun produce grammar stateset i indata =
   (case Array.sub (stateset, i) of