1.1 --- a/src/Pure/library.ML	Thu Jun 05 13:28:32 1997 +0200
     1.2 +++ b/src/Pure/library.ML	Thu Jun 05 13:29:41 1997 +0200
     1.3 @@ -370,9 +370,10 @@
     1.4    in implode (map chrof (radixpand (base, num))) end;
     1.5  
     1.6  
     1.7 -fun string_of_int n =
     1.8 -  if n < 0 then "~" ^ radixstring (10, "0", ~n) else radixstring (10, "0", n);
     1.9 +val string_of_int = Int.toString;
    1.10  
    1.11 +fun string_of_indexname (a,0) = a
    1.12 +  | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;
    1.13  
    1.14  
    1.15  (** strings **)