# HG changeset patch
# User wenzelm
# Date 1752235975 -7200
# Node ID bec9aa9734478399c0b2bcf099f4e4ffeaca7cac
# Parent  8aa1c98b948b335e32bb96394f8b03004cea8239
clarified print order: follow original classical.ML, before 8aa1c98b948b;

diff -r 8aa1c98b948b -r bec9aa973447 src/Pure/bires.ML
--- a/src/Pure/bires.ML	Fri Jul 11 14:03:09 2025 +0200
+++ b/src/Pure/bires.ML	Fri Jul 11 14:12:55 2025 +0200
@@ -192,7 +192,7 @@
   kinds |> map (fn kind =>
     Pretty.big_list (kind_title kind ^ ":")
       (dest_decls (fn (_, {kind = kind', ...}) => kind = kind') decls
-        |> sort (tag_ord o apply2 (#tag o #2))
+        |> sort (decl_ord o apply2 #2)
         |> map (fn (th, _) => Thm.pretty_thm_item ctxt th)));
 
 fun merge_decls (decls1, decls2) =