# HG changeset patch
# User wenzelm
# Date 1594807003 -7200
# Node ID 452073b64f28e2b73df1ef20f0ec90263cc2b55e
# Parent  70bfda10f597946159dbc7071a13f42f0f432042
clarified signature;

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 */