# HG changeset patch
# User wenzelm
# Date 1683279416 -7200
# Node ID d4184ea197ece5dafac2a49e961638d99b40e8ca
# Parent  3a97b5bff51a837c4493332adbe657f7f2794bfa
tuned signature;

diff -r 3a97b5bff51a -r d4184ea197ec src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Fri May 05 11:29:27 2023 +0200
+++ b/src/Pure/General/long_name.ML	Fri May 05 11:36:56 2023 +0200
@@ -31,7 +31,7 @@
   val make_chunks: string -> chunks
   val explode_chunks: chunks -> string list
   val implode_chunks: chunks -> string
-  val compare_chunks: chunks * chunks -> order
+  val compare_chunks: chunks ord
   val eq_chunks: chunks * chunks -> bool
   structure Chunks: CHANGE_TABLE
 end;
diff -r 3a97b5bff51a -r d4184ea197ec src/Pure/library.ML
--- a/src/Pure/library.ML	Fri May 05 11:29:27 2023 +0200
+++ b/src/Pure/library.ML	Fri May 05 11:36:56 2023 +0200
@@ -198,7 +198,7 @@
   val is_greater_equal: order -> bool
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a ord
-  val pointer_eq_ord: ('a * 'a -> order) -> 'a * 'a -> order
+  val pointer_eq_ord: 'a ord -> 'a ord
   val bool_ord: bool ord
   val int_ord: int ord
   val string_ord: string ord