tuned;

--- a/src/Pure/System/invoke_scala.scala	Sat Apr 29 20:30:13 2017 +0200
+++ b/src/Pure/System/invoke_scala.scala	Sat Apr 29 20:34:46 2017 +0200
@@ -46,11 +46,7 @@
 
   object Tag extends Enumeration
   {
-    val NULL = Value("0")
-    val OK = Value("1")
-    val ERROR = Value("2")
-    val FAIL = Value("3")
-    val INTERRUPT = Value("4")
+    val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
   def method(name: String, arg: String): (Tag.Value, String) =
@@ -87,7 +83,7 @@
     synchronized
     {
       if (futures.isDefinedAt(id)) {
-        session.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
+        session.protocol_command("Invoke_Scala.fulfill", id, tag.id.toString, res)
         futures -= id
       }
     }