sym: Symbol.output_width;

--- a/src/Pure/General/pretty.ML	Thu Feb 11 21:15:27 1999 +0100
+++ b/src/Pure/General/pretty.ML	Thu Feb 11 21:15:46 1999 +0100
@@ -149,7 +149,7 @@
 
 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);