# HG changeset patch
# User berghofe
# Date 1082134093 -7200
# Node ID ba51bc23971607aa983dd793ee34005dfb5fc970
# Parent  c3177fffd31a8441a58c32c83d5fe17dc3b20a7d
Replaced quote by Pretty.quote / Library.quote, since quote now refers to Symbol.quote

diff -r c3177fffd31a -r ba51bc239716 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Apr 16 18:47:00 2004 +0200
+++ b/src/Pure/Syntax/parser.ML	Fri Apr 16 18:48:13 2004 +0200
@@ -397,14 +397,14 @@
 
     val taglist = Symtab.dest tags;
 
-    fun pretty_symb (Terminal (Token s)) = Pretty.str (quote s)
+    fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s)
       | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
       | pretty_symb (Nonterminal (tag, p)) =
         let val name = fst (the (find_first (fn (n, t) => t = tag) taglist));
         in Pretty.str (name ^ "[" ^ string_of_int p ^ "]") end;
 
     fun pretty_const "" = []
-      | pretty_const c = [Pretty.str ("=> " ^ quote c)];
+      | pretty_const c = [Pretty.str ("=> " ^ Library.quote c)];
 
     fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];