# HG changeset patch
# User wenzelm
# Date 1203000326 -3600
# Node ID 3d2a4fd4ed7759051b1ae517910eda55e3a5f555
# Parent  728f2c325ed6a15f44c8716c9bd0cf3375328a99
expected syntax categories: reduced duplication, report minimal priorities only;

diff -r 728f2c325ed6 -r 3d2a4fd4ed77 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Thu Feb 14 01:31:30 2008 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Feb 14 15:45:26 2008 +0100
@@ -795,7 +795,8 @@
 
         val nt_name = reverted_tags tags;
         val nts =
-          fold (fn (_, _, _, Nonterminal nt :: _, _, _) => insert (op =) nt | _ => I)
+          fold (fn (_, _, _, Nonterminal (tag, p) :: _, _, _) =>
+            AList.map_default (op =) (tag, p) (fn p' => Int.min (p, p')) | _ => I)
             (Array.sub (stateset, i - 1)) []
           |> map (fn (a, prec) => nt_name a ^ "[" ^ signed_string_of_int prec ^ "]");