tuned;

--- a/src/Pure/General/latex.ML	Fri Oct 25 22:22:21 2024 +0200
+++ b/src/Pure/General/latex.ML	Sat Oct 26 16:07:03 2024 +0200
@@ -170,8 +170,7 @@
 
 in
 
-val length_symbols =
-  Integer.build o fold Integer.add o these o read scan_latex_length;
+val length_symbols = Integer.sum o these o read scan_latex_length;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then