# HG changeset patch
# User paulson
# Date 865510181 -7200
# Node ID afd288caf5739b1c977de4749505151a8455dc58
# Parent  131262e21ada3f35c71c90f093126ec58ca01c35
Removal of radixstring from string_of_int; addition of string_of_indexname

diff -r 131262e21ada -r afd288caf573 src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Jun 05 13:28:32 1997 +0200
+++ b/src/Pure/library.ML	Thu Jun 05 13:29:41 1997 +0200
@@ -370,9 +370,10 @@
   in implode (map chrof (radixpand (base, num))) end;
 
 
-fun string_of_int n =
-  if n < 0 then "~" ^ radixstring (10, "0", ~n) else radixstring (10, "0", n);
+val string_of_int = Int.toString;
 
+fun string_of_indexname (a,0) = a
+  | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
 
 
 (** strings **)