--- a/src/Pure/Syntax/parser.ML Wed Oct 27 11:13:25 1999 +0200
+++ b/src/Pure/Syntax/parser.ML Wed Oct 27 11:15:35 1999 +0200
@@ -792,7 +792,7 @@
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 Symbol.output o str_of_token)
+ Pretty.breaks (map (Pretty.str o str_of_token)
(rev (tl (rev toks)))) @
[Pretty.str "\""]);
val expected =
--- a/src/Pure/Syntax/syntax.ML Wed Oct 27 11:13:25 1999 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Oct 27 11:15:35 1999 +0200
@@ -353,12 +353,11 @@
val chars = Symbol.explode str;
val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
- fun show_pt pt =
- warning (Symbol.output (Pretty.string_of
- (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt))));
+ fun show_pt pt = warning (Pretty.string_of
+ (Ast.pretty_ast (SynTrans.pt_to_ast (K None) pt)));
in
if length pts > ! ambiguity_level then
- (warning ("Ambiguous input " ^ quote (Symbol.output str));
+ (warning ("Ambiguous input " ^ quote str);
warning "produces the following parse trees:";
seq show_pt pts)
else ();