# HG changeset patch
# User wenzelm
# Date 918764146 -3600
# Node ID 957d8aa4a06bee804c5a97dd164068243f92eefe
# Parent  c905fe5994a2a83102f93bad642b3ce63668c92e
sym: Symbol.output_width;

diff -r c905fe5994a2 -r 957d8aa4a06b src/Pure/General/pretty.ML
--- 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);