clarified signature;

--- 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
   }
 

--- a/src/Pure/library.scala	Mon Apr 12 22:18:37 2021 +0200
+++ b/src/Pure/library.scala	Mon Apr 12 22:26:09 2021 +0200
@@ -275,6 +275,12 @@
       res.toList
     }
 
+  def the_single[A](xs: List[A]): A =
+    xs match {
+      case List(x) => x
+      case _ => error("Single argument expected")
+    }
+
 
   /* proper values */