1.1 --- a/src/Pure/General/pretty.ML	Thu Feb 11 21:15:27 1999 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Thu Feb 11 21:15:46 1999 +0100
     1.3 @@ -149,7 +149,7 @@
     1.4  
     1.5  fun str s = String (s, size s);
     1.6  fun strlen s len = String (s, len);
     1.7 -fun sym s = String (s, Symbol.size s);
     1.8 +val sym = String o apsnd Real.round o Symbol.output_width;
     1.9  
    1.10  fun spc n = str (repstring " " n);
    1.11