src/Pure/General/pretty.ML

   | length (String (_, len)) = len
   | length (Break(_, wd)) = wd;
 
 fun str s = String (s, size s);
 fun strlen s len = String (s, len);
-fun sym s = String (s, Symbol.size s);
+val sym = String o apsnd Real.round o Symbol.output_width;
 
 fun spc n = str (repstring " " n);
 
 fun brk wd = Break (false, wd);
 val fbrk = Break (true, 0);