diff -r e21aef453cd4 -r f86661e32bed src/Pure/System/scala.scala --- 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 }