# HG changeset patch
# User wenzelm
# Date 1120672839 -7200
# Node ID e264077b68a70304ea160469469c3ad7300b02f2
# Parent  4399016bf13e3eb78c8c5b89b451b0dd950d48aa
dest_parsers: sort result;

diff -r 4399016bf13e -r e264077b68a7 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 06 20:00:37 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 06 20:00:39 2005 +0200
@@ -216,8 +216,8 @@
 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
 
 fun dest_parsers () =
-  map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
-    (Symtab.dest (get_parsers ()));
+  get_parsers () |> Symtab.dest |> sort_wrt #1
+  |> map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only));
 
 fun print_outer_syntax () =
   let