--- 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;
--- 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