# HG changeset patch
# User wenzelm
# Date 1201385733 -3600
# Node ID bfda3f3beccd1317822b8c667b5d61ac41167f10
# Parent  26f1e4c172c3640efec1b685c0ff54babc17a8fb
syntax error: unified output of priorities;

diff -r 26f1e4c172c3 -r bfda3f3beccd src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Jan 26 22:14:07 2008 +0100
+++ b/src/Pure/Syntax/parser.ML	Sat Jan 26 23:15:33 2008 +0100
@@ -797,7 +797,7 @@
         val nts =
           fold (fn (_, _, _, Nonterminal nt :: _, _, _) => insert (op =) nt | _ => I)
             (Array.sub (stateset, i - 1)) []
-          |> map (fn (a, prec) => nt_name a ^ "(" ^ signed_string_of_int prec ^ ")");
+          |> map (fn (a, prec) => nt_name a ^ "[" ^ signed_string_of_int prec ^ "]");
 
         val msg =
           (if null toks then Pretty.str "Inner syntax error: unexpected end of input"