--- a/src/Pure/General/position.ML Fri Sep 27 20:29:38 2024 +0200
+++ b/src/Pure/General/position.ML Fri Sep 27 22:08:54 2024 +0200
@@ -61,6 +61,7 @@
val here: T -> string
val here_list: T list -> string
type range = T * T
+ val range_ord: range ord
val no_range: range
val no_range_position: T -> T
val range_position: range -> T
@@ -299,6 +300,8 @@
type range = T * T;
+val range_ord = prod_ord ord ord;
+
val no_range = (none, none);
fun no_range_position (Pos {line, offset, end_offset = _, props}) =