corrected output of symbols for several (probably not all) relevant functions

--- a/src/Pure/Syntax/parser.ML	Fri Jan 29 17:10:26 1999 +0100
+++ b/src/Pure/Syntax/parser.ML	Fri Jan 29 17:11:40 1999 +0100
@@ -792,7 +792,8 @@
       if null toks then Pretty.str "Inner syntax error: unexpected end of input"
       else
         Pretty.block (Pretty.str "Inner syntax error at: \"" ::
-          Pretty.breaks (map (Pretty.str o str_of_token) (rev (tl (rev toks)))) @
+          Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token)
+		 (rev (tl (rev toks)))) @
           [Pretty.str "\""]);
     val expected =
       Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed);