# HG changeset patch
# User wenzelm
# Date 1227029155 -3600
# Node ID 1987ef778a025e45e2eea26eba5b6adb34a4f015
# Parent  e44fae2b721dafb577ba4e66fe66a9ce97b25ede
signed_string_of_int for priorities;
tuned;

diff -r e44fae2b721d -r 1987ef778a02 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue Nov 18 18:25:52 2008 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Nov 18 18:25:55 2008 +0100
@@ -397,12 +397,13 @@
 
     fun pretty_symb (Terminal (Token (Literal, s, _))) = Pretty.quote (Pretty.str s)
       | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
-      | pretty_symb (Nonterminal (tag, p)) = Pretty.str (nt_name tag ^ "[" ^ string_of_int p ^ "]");
+      | pretty_symb (Nonterminal (tag, p)) =
+          Pretty.str (nt_name tag ^ "[" ^ signed_string_of_int p ^ "]");
 
     fun pretty_const "" = []
-      | pretty_const c = [Pretty.str ("=> " ^ Library.quote c)];
+      | pretty_const c = [Pretty.str ("=> " ^ quote c)];
 
-    fun pretty_pri p = [Pretty.str ("(" ^ string_of_int p ^ ")")];
+    fun pretty_pri p = [Pretty.str ("(" ^ signed_string_of_int p ^ ")")];
 
     fun pretty_prod name (symbs, const, pri) =
       Pretty.block (Pretty.breaks (pretty_name name @