# HG changeset patch
# User wenzelm
# Date 1683235859 -7200
# Node ID 01e04f024bb5f2dbade7ab6b39ccaabda6b31328
# Parent  93d2b378695929f73503c266ea9e0e37e544093f
revert pointless performance tuning fd5f4455e033: no measurable difference in HOL, HOL-Library, HOL-Analysis;

diff -r 93d2b3786959 -r 01e04f024bb5 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Thu May 04 17:29:54 2023 +0200
+++ b/src/Pure/General/long_name.ML	Thu May 04 23:30:59 2023 +0200
@@ -113,21 +113,21 @@
 
 in
 
-abstype chunks = Chunks of {range0: int, ranges: int vector (*reverse*), string: string}
+abstype chunks = Chunks of {range0: int, ranges: int list (*reverse*), string: string}
 with
 
-val empty_chunks = Chunks {range0 = range_empty, ranges = ranges_empty, string = ""};
+val empty_chunks = Chunks {range0 = range_empty, ranges = [], string = ""};
 
 fun is_empty_chunks (Chunks {range0, ranges, ...}) =
-  range0 = range_empty andalso Vector.length ranges = 0;
+  range0 = range_empty andalso null ranges;
 
 fun count_chunks (chunks as Chunks {ranges, ...}) =
   if is_empty_chunks chunks then 0
-  else Vector.length ranges + 1;
+  else length ranges + 1;
 
 fun size_chunks (chunks as Chunks {range0, ranges, ...}) =
   if is_empty_chunks chunks then 0
-  else Vector.fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
+  else fold (fn r => fn n => n + range_length r + 1) ranges (range_length range0);
 
 fun base_chunks name =
   let
@@ -135,7 +135,7 @@
     val j = i + 1;
   in
     if i < 0 then empty_chunks
-    else Chunks {range0 = range name j (size name - j), ranges = ranges_empty, string = name}
+    else Chunks {range0 = range name j (size name - j), ranges = [], string = name}
   end;
 
 fun suppress_chunks suppress1 suppress2 string =
@@ -170,7 +170,7 @@
         else
           (case rs' of
             [] => empty_chunks
-          | r0 :: rest => Chunks {range0 = r0, ranges = Vector.fromList rest, string = string})
+          | r0 :: rest => Chunks {range0 = r0, ranges = rest, string = string})
       end;
   in suppr_chunks suppress1 suppress2 0 0 [] end;
 
@@ -178,11 +178,11 @@
 
 fun explode_chunks (chunks as Chunks {range0, ranges, string}) =
   if is_empty_chunks chunks then []
-  else Vector.fold (cons o range_string string) ranges [range_string string range0];
+  else fold (cons o range_string string) ranges [range_string string range0];
 
 fun implode_chunks (chunks as Chunks {range0, ranges, string}) =
   if size_chunks chunks = size string then string
-  else if Vector.length ranges = 0 then range_string string range0
+  else if null ranges then range_string string range0
   else implode (explode_chunks chunks);
 
 val compare_chunks = pointer_eq_ord (fn (chunks1, chunks2) =>
@@ -212,10 +212,10 @@
         EQUAL =>
           (case range_length_ord (range01, range02) of
             EQUAL =>
-              (case Vector.collate range_length_ord (ranges1, ranges2) of
+              (case dict_ord range_length_ord (ranges1, ranges2) of
                 EQUAL =>
                   (case range_substring_ord (range01, range02) of
-                    EQUAL => Vector.collate range_substring_ord (ranges1, ranges2)
+                    EQUAL => dict_ord range_substring_ord (ranges1, ranges2)
                   | ord => ord)
               | ord => ord)
           | ord => ord)