# HG changeset patch
# User wenzelm
# Date 1546515266 -3600
# Node ID b4ea943ce0b7f63e43d914e783bac46455bf74b1
# Parent  c7a69b6cd405ab4c9d2c23378e4950f22ccf9dfc
tuned;

diff -r c7a69b6cd405 -r b4ea943ce0b7 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Wed Jan 02 21:18:35 2019 +0100
+++ b/src/Pure/PIDE/xml.ML	Thu Jan 03 12:34:26 2019 +0100
@@ -294,7 +294,7 @@
 
 (* atomic values *)
 
-fun int_atom i = signed_string_of_int i;
+fun int_atom i = Value.print_int i;
 
 fun bool_atom false = "0"
   | bool_atom true = "1";
diff -r c7a69b6cd405 -r b4ea943ce0b7 src/Pure/config.ML
--- a/src/Pure/config.ML	Wed Jan 02 21:18:35 2019 +0100
+++ b/src/Pure/config.ML	Thu Jan 03 12:34:26 2019 +0100
@@ -46,7 +46,7 @@
 
 fun print_value (Bool true) = "true"
   | print_value (Bool false) = "false"
-  | print_value (Int i) = signed_string_of_int i
+  | print_value (Int i) = Value.print_int i
   | print_value (Real x) = Value.print_real x
   | print_value (String s) = quote s;