# HG changeset patch
# User wenzelm
# Date 1729951623 -7200
# Node ID a477ce2fe491bbfe03c75561f30c39fb199b4f58
# Parent  d912f97aaa861e806011456ac18058f55b93f028
tuned;

diff -r d912f97aaa86 -r a477ce2fe491 src/Pure/General/latex.ML
--- 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