src/Pure/System/scala.scala
changeset 73571 f86661e32bed
parent 73565 1aa92bc4d356
child 73576 b50f8cc8c08e
--- a/src/Pure/System/scala.scala	Mon Apr 12 22:18:37 2021 +0200
+++ b/src/Pure/System/scala.scala	Mon Apr 12 22:26:09 2021 +0200
@@ -39,10 +39,7 @@
   {
     override def multi: Boolean = false
     override def apply(args: List[String]): List[String] =
-      args match {
-        case List(arg) => List(apply(arg))
-        case _ => error("Expected single argument for Scala function " + quote(name))
-      }
+      List(apply(Library.the_single(args)))
     def apply(arg: String): String
   }