# HG changeset patch
# User wenzelm
# Date 1683536958 -7200
# Node ID fdb71efcc04afc9cc3d65978f235f30dd2697684
# Parent  1de3db73618efff1d19a034d355f75e89d49030f
tuned;

diff -r 1de3db73618e -r fdb71efcc04a src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Mon May 08 11:09:13 2023 +0200
+++ b/src/Pure/General/long_name.ML	Mon May 08 11:09:18 2023 +0200
@@ -108,18 +108,15 @@
 fun range_length r = r mod range_limit;
 fun range_string s r = String.substring (s, range_index r, range_length r);
 
-val range_empty = 0;
-val ranges_empty: int vector = Vector.fromList [];
-
 in
 
 abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
 with
 
-val empty_chunks = Chunks {range0 = range_empty, ranges = [], string = ""};
+val empty_chunks = Chunks {range0 = 0, ranges = [], string = ""};
 
 fun is_empty_chunks (Chunks {range0, ranges, ...}) =
-  range0 = range_empty andalso null ranges;
+  range0 = 0 andalso null ranges;
 
 fun count_chunks (chunks as Chunks {ranges, ...}) =
   if is_empty_chunks chunks then 0