src/Pure/Thy/latex.ML

 fun read scan syms =
   Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
 
 in
 
-fun length_symbols syms =
-  fold Integer.add (these (read scan_latex_length syms)) 0;
+val length_symbols =
+  Integer.build o fold Integer.add o these o read scan_latex_length;
 
 fun output_symbols syms =
   if member (op =) syms Symbol.latex then
     (case read scan_latex syms of
       SOME ss => implode ss