tuned string_of_int to avoid allocation for small integers;

--- a/src/Pure/library.ML	Mon Jan 10 15:45:46 2011 +0100
+++ b/src/Pure/library.ML	Mon Jan 10 16:07:16 2011 +0100
@@ -642,7 +642,19 @@
   in implode (map chrof (radixpand (base, num))) end;
 
 
-val string_of_int = Int.toString;
+local
+  val zero = ord "0";
+  val small = 10000;
+  val small_table = Vector.tabulate (small, Int.toString);
+in
+
+fun string_of_int i =
+  if i < 0 then Int.toString i
+  else if i < 10 then chr (zero + i)
+  else if i < small then Vector.sub (small_table, i)
+  else Int.toString i;
+
+end;
 
 fun signed_string_of_int i =
   if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;