corrected output of symbols for several (probably not all) relevant functions
authoroheimb
Fri Jan 29 17:11:40 1999 +0100 (1999-01-29)
changeset 6165a7d74bf9da52
parent 6164 a0e9501d56f8
child 6166 a56aaad7ff2d
corrected output of symbols for several (probably not all) relevant functions
src/Pure/Syntax/parser.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Fri Jan 29 17:10:26 1999 +0100
     1.2 +++ b/src/Pure/Syntax/parser.ML	Fri Jan 29 17:11:40 1999 +0100
     1.3 @@ -792,7 +792,8 @@
     1.4        if null toks then Pretty.str "Inner syntax error: unexpected end of input"
     1.5        else
     1.6          Pretty.block (Pretty.str "Inner syntax error at: \"" ::
     1.7 -          Pretty.breaks (map (Pretty.str o str_of_token) (rev (tl (rev toks)))) @
     1.8 +          Pretty.breaks (map (Pretty.str o Symbol.output o str_of_token)
     1.9 +		 (rev (tl (rev toks)))) @
    1.10            [Pretty.str "\""]);
    1.11      val expected =
    1.12        Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed);