pretty_gram: now sorts productions;

--- 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;