author | wenzelm |
Fri, 29 Dec 2006 18:46:04 +0100 | |
changeset 21944 | e877a5a78522 |
parent 21943 | b7b66f440d04 |
child 21945 | 4dd9a5fc7fc3 |
--- 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