clarified print order: follow original classical.ML, before 8aa1c98b948b;
authorwenzelm
Fri, 11 Jul 2025 14:12:55 +0200
changeset 82843 bec9aa973447
parent 82842 8aa1c98b948b
child 82844 ebfb0e011c95
clarified print order: follow original classical.ML, before 8aa1c98b948b;
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) =