# HG changeset patch
# User wenzelm
# Date 1167414362 -3600
# Node ID d6218d0f9ec31ce2cf7859eb5135a5b4b3f9fc27
# Parent  62dd79056d706ea9fd9dc115d0dfeb8ca6f776d4
added signed_string_of_int (pruduces proper - instead of SML's ~);

diff -r 62dd79056d70 -r d6218d0f9ec3 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 29 18:46:01 2006 +0100
+++ b/src/Pure/library.ML	Fri Dec 29 18:46:02 2006 +0100
@@ -136,6 +136,7 @@
   val radixpand: int * int -> int list
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
+  val signed_string_of_int: int -> string
   val string_of_indexname: string * int -> string
   val read_intinf: int -> string list -> IntInf.int * string list
   val read_int: string list -> int * string list
@@ -705,6 +706,9 @@
 
 val string_of_int = Int.toString;
 
+fun signed_string_of_int i =
+  if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
+
 fun string_of_indexname (a,0) = a
   | string_of_indexname (a,i) = a ^ "_" ^ Int.toString i;