# HG changeset patch
# User wenzelm
# Date 1727633488 -7200
# Node ID 7846fa2c1c1ed589885d3a248b2b09c2b143cecd
# Parent  07ad0b407d38066e7aa2261f198f3bc2e95ec8dc
clarified order for 'print_syntax' command;

diff -r 07ad0b407d38 -r 7846fa2c1c1e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Sep 29 19:51:23 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 29 20:11:28 2024 +0200
@@ -399,7 +399,7 @@
 
 type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
 
-fun dest_ruletab tab = maps snd (Symtab.dest tab);
+fun dest_ruletab tab = Symtab.dest tab |> sort_by #1 |> maps #2;
 
 val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
 val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));