# HG changeset patch
# User wenzelm
# Date 789827123 -3600
# Node ID 5e59370243fa9f665e8d74e330f6172176af0bdf
# Parent  c1a4a42061025c41b6854e9479cde5e3e26fce84
pretty_gram: now sorts productions;

diff -r c1a4a4206102 -r 5e59370243fa src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Jan 11 10:57:39 1995 +0100
+++ b/src/Pure/Syntax/parser.ML	Wed Jan 11 13:25:23 1995 +0100
@@ -304,7 +304,7 @@
       Pretty.block (Pretty.breaks (pretty_name name @
         map pretty_symb symbs @ pretty_const const @ pretty_pri pri));
   in
-    map pretty_prod prods
+    map pretty_prod (sort (op <= o pairself #1) prods)
   end;