diff -r 3f9ef4bf3f31 -r 25c84ca5e9a9 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 05 22:46:58 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 05 22:46:59 2007 +0200
@@ -84,8 +84,9 @@
 
 fun print_antiquotations () =
  [Pretty.big_list "text antiquotation commands:"
-    (map Pretty.str (Symtab.keys (! global_commands))),
-  Pretty.big_list "text antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))]
+    (map Pretty.str (sort_strings (Symtab.keys (! global_commands)))),
+  Pretty.big_list "text antiquotation options:"
+    (map Pretty.str (sort_strings (Symtab.keys (! global_options))))]
  |> Pretty.chunks |> Pretty.writeln;
 
 end;