author | wenzelm |
Fri, 11 Jul 2025 14:12:55 +0200 | |
changeset 82843 | bec9aa973447 |
parent 82842 | 8aa1c98b948b |
child 82844 | ebfb0e011c95 |
src/Pure/bires.ML | file | annotate | diff | comparison | revisions |
--- 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) =