| changeset 69574 | b4ea943ce0b7 |
| parent 68827 | 1286ca9dfd26 |
| child 69575 | f77cc54f6d47 |
--- 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;