# HG changeset patch
# User wenzelm
# Date 1167414364 -3600
# Node ID e877a5a78522d916165ac6223f37cc5afcf1b0e6
# Parent  b7b66f440d04d88dfa7d997e9a06f89de05f26b0
signed_string_of_int;

diff -r b7b66f440d04 -r e877a5a78522 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 29 18:46:04 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Fri Dec 29 18:46:04 2006 +0100
@@ -215,8 +215,7 @@
        | NONE => raise PGIP ("Expected a non-empty string: "^s))
     handle _ => raise PGIP ("Invalid XML string syntax: "^s)
 
-fun int_to_pgstring i =
-  if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i
+val int_to_pgstring = signed_string_of_int
 
 fun string_to_pgstring s = XML.text s