diff -r 70bfda10f597 -r 452073b64f28 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Mon Jul 13 23:23:35 2020 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Wed Jul 15 11:56:43 2020 +0200
@@ -9,13 +9,14 @@
 
 object ML_Syntax
 {
-  /* int */
+  /* numbers */
 
-  private def signed_int(s: String): String =
+  private def signed(s: String): String =
     if (s(0) == '-') "~" + s.substring(1) else s
 
-  def print_int(i: Int): String = signed_int(Value.Int(i))
-  def print_long(i: Long): String = signed_int(Value.Long(i))
+  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 */