diff --git a/src/Pure/General/space.scala b/src/Pure/General/space.scala
--- a/src/Pure/General/space.scala
+++ b/src/Pure/General/space.scala
@@ -1,56 +1,56 @@
 /*  Title:      Pure/General/space.scala
     Author:     Makarius
 
 Storage space based on bytes.
 */
 
 package isabelle
 
 
 import java.util.Locale
 
 import scala.annotation.tailrec
 
 
 object Space {
   def bytes(bs: Long): Space = new Space(bs)
   val zero: Space = bytes(0L)
 
   private val units: List[String] = List("B", "KiB", "MiB", "GiB", "TiB", "PiB", "EiB")
 
   def B(x: Double): Space = bytes(x.round)
   def KiB(x: Double): Space = B(x * 1024)
   def MiB(x: Double): Space = KiB(x * 1024)
   def GiB(x: Double): Space = MiB(x * 1024)
   def TiB(x: Double): Space = GiB(x * 1024)
   def PiB(x: Double): Space = TiB(x * 1024)
   def EiB(x: Double): Space = PiB(x * 1024)
 }
 
 final class Space private(val bytes: Long) extends AnyVal {
   def is_proper: Boolean = bytes > 0
   def is_relevant: Boolean = MiB >= 1.0
 
   def B: Double = bytes.toDouble
   def KiB: Double = B / 1024
   def MiB: Double = KiB / 1024
   def GiB: Double = MiB / 1024
   def TiB: Double = GiB / 1024
   def PiB: Double = TiB / 1024
   def EiB: Double = PiB / 1024
 
-  override def toString: String = bytes.toString
+  override def toString: String = Value.Long(bytes)
 
   def print: String = {
     @tailrec def print_unit(x: Double, units: List[String]): String =
       if (x.abs < 1024 || units.tail.isEmpty) {
         val s = String.format(Locale.ROOT, "%.1f", x.asInstanceOf[AnyRef])
         Library.perhaps_unsuffix(".0", s) + " " + units.head
       }
       else print_unit(x / 1024, units.tail)
 
     print_unit(bytes.toDouble, Space.units)
   }
 
   def print_relevant: Option[String] = if (is_relevant) Some(print) else None
 }
diff --git a/src/Pure/ML/ml_syntax.scala b/src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala
+++ b/src/Pure/ML/ml_syntax.scala
@@ -1,65 +1,65 @@
 /*  Title:      Pure/ML/ml_syntax.scala
     Author:     Makarius
 
 Concrete ML syntax for basic values.
 */
 
 package isabelle
 
 
 object ML_Syntax {
   /* numbers */
 
   private def signed(s: String): String =
     if (s(0) == '-') "~" + s.substring(1) else s
 
   def print_int(x: Int): String = signed(Value.Int(x))
   def print_long(x: Long): String = signed(Value.Long(x))
   def print_double(x: Double): String = signed(Value.Double(x))
 
 
   /* string */
 
   private def print_byte(c: Byte): String =
     c match {
       case 34 => "\\\""
       case 92 => "\\\\"
       case 9 => "\\t"
       case 10 => "\\n"
       case 12 => "\\f"
       case 13 => "\\r"
       case _ =>
-        if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
+        if (c < 0) "\\" + Value.Int(256 + c)
         else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
         else if (c < 127) Symbol.ascii(c.toChar)
-        else "\\" + Library.signed_string_of_int(c)
+        else "\\" + Value.Int(c)
     }
 
   private def print_symbol(s: Symbol.Symbol): String =
     if (s.startsWith("\\<")) s
     else UTF8.bytes(s).iterator.map(print_byte).mkString
 
   def print_string_bytes(str: String): String =
     quote(UTF8.bytes(str).iterator.map(print_byte).mkString)
 
   def print_string_symbols(str: String): String =
     quote(Symbol.iterator(str).map(print_symbol).mkString)
 
 
   /* pair */
 
   def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
     "(" + f(pair._1) + ", " + g(pair._2) + ")"
 
 
   /* list */
 
   def print_list[A](f: A => String)(list: List[A]): String =
     "[" + commas(list.map(f)) + "]"
 
 
   /* properties */
 
   def print_properties(props: Properties.T): String =
     print_list(print_pair(print_string_bytes, print_string_bytes))(props)
 }