diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala
+++ b/src/Pure/System/scala.scala
@@ -1,285 +1,282 @@
 /*  Title:      Pure/System/scala.scala
     Author:     Makarius
 
 Support for Scala at runtime.
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, StringWriter, PrintWriter}
 
 import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter}
 import scala.tools.nsc.interpreter.{IMain, Results}
 import scala.tools.nsc.interpreter.shell.ReplReporterImpl
 
 object Scala
 {
   /** registered functions **/
 
   abstract class Fun(val name: String, val thread: Boolean = false)
   {
     override def toString: String = name
     def multi: Boolean = true
     def position: Properties.T = here.position
     def here: Scala_Project.Here
     def invoke(args: List[Bytes]): List[Bytes]
   }
 
   abstract class Fun_Strings(name: String, thread: Boolean = false)
     extends Fun(name, thread = thread)
   {
     override def invoke(args: List[Bytes]): List[Bytes] =
       apply(args.map(_.text)).map(Bytes.apply)
     def apply(args: List[String]): List[String]
   }
 
   abstract class Fun_String(name: String, thread: Boolean = false)
     extends Fun_Strings(name, thread = thread)
   {
     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
   }
 
   class Functions(val functions: Fun*) extends Isabelle_System.Service
 
   lazy val functions: List[Fun] =
     Isabelle_System.make_services(classOf[Functions]).flatMap(_.functions)
 
 
 
   /** demo functions **/
 
   object Echo extends Fun_String("echo")
   {
     val here = Scala_Project.here
     def apply(arg: String): String = arg
   }
 
   object Sleep extends Fun_String("sleep")
   {
     val here = Scala_Project.here
     def apply(seconds: String): String =
     {
       val t =
         seconds match {
           case Value.Double(s) => Time.seconds(s)
           case _ => error("Malformed argument: " + quote(seconds))
         }
       val t0 = Time.now()
       t.sleep
       val t1 = Time.now()
       (t1 - t0).toString
     }
   }
 
 
 
   /** compiler **/
 
   object Compiler
   {
     def context(
       error: String => Unit = Exn.error,
       jar_dirs: List[JFile] = Nil): Context =
     {
       def find_jars(dir: JFile): List[String] =
         File.find_files(dir, file => file.getName.endsWith(".jar")).
           map(File.absolute_name)
 
       val class_path =
         for {
           prop <- List("isabelle.scala.classpath", "java.class.path")
           path = System.getProperty(prop, "") if path != "\"\""
           elem <- space_explode(JFile.pathSeparatorChar, path)
         } yield elem
 
       val settings = new GenericRunnerSettings(error)
       settings.classpath.value =
         (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
       new Context(settings)
     }
 
     def default_print_writer: PrintWriter =
       new NewLinePrintWriter(new ConsoleWriter, true)
 
     class Context private [Compiler](val settings: GenericRunnerSettings)
     {
       override def toString: String = settings.toString
 
       def interpreter(
         print_writer: PrintWriter = default_print_writer,
         class_loader: ClassLoader = null): IMain =
       {
         new IMain(settings, new ReplReporterImpl(settings, print_writer))
         {
           override def parentClassLoader: ClassLoader =
             if (class_loader == null) super.parentClassLoader
             else class_loader
         }
       }
 
       def toplevel(interpret: Boolean, source: String): List[String] =
       {
         val out = new StringWriter
         val interp = interpreter(new PrintWriter(out))
         val marker = '\u000b'
         val ok =
           interp.withLabel(marker.toString) {
             if (interpret) interp.interpret(source) == Results.Success
             else (new interp.ReadEvalPrint).compile(source)
           }
         out.close()
 
         val Error = """(?s)^\S* error: (.*)$""".r
         val errors =
           space_explode(marker, Library.strip_ansi_color(out.toString)).
             collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
         if (!ok && errors.isEmpty) List("Error") else errors
       }
     }
   }
 
   object Toplevel extends Fun_String("scala_toplevel")
   {
     val here = Scala_Project.here
     def apply(arg: String): String =
     {
       val (interpret, source) =
         YXML.parse_body(arg) match {
           case Nil => (false, "")
           case List(XML.Text(source)) => (false, source)
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
         try { Compiler.context().toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
   }
 
 
 
   /** invoke Scala functions from ML **/
 
   /* invoke function */
 
   object Tag extends Enumeration
   {
     val NULL, OK, ERROR, FAIL, INTERRUPT = Value
   }
 
   def function_thread(name: String): Boolean =
     functions.find(fun => fun.name == name) match {
       case Some(fun) => fun.thread
       case None => false
     }
 
   def function_body(name: String, args: List[Bytes]): (Tag.Value, List[Bytes]) =
     functions.find(fun => fun.name == name) match {
       case Some(fun) =>
         Exn.capture { fun.invoke(args) } match {
           case Exn.Res(null) => (Tag.NULL, Nil)
           case Exn.Res(res) => (Tag.OK, res)
           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, Nil)
           case Exn.Exn(e) => (Tag.ERROR, List(Bytes(Exn.message(e))))
         }
       case None => (Tag.FAIL, List(Bytes("Unknown Isabelle/Scala function: " + quote(name))))
     }
 
 
   /* protocol handler */
 
   class Handler extends Session.Protocol_Handler
   {
     private var session: Session = null
     private var futures = Map.empty[String, Future[Unit]]
 
     override def init(session: Session): Unit =
       synchronized { this.session = session }
 
     override def exit(): Unit = synchronized
     {
       for ((id, future) <- futures) cancel(id, future)
       futures = Map.empty
     }
 
     private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
       synchronized
       {
         if (futures.isDefinedAt(id)) {
           session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
           futures -= id
         }
       }
 
     private def cancel(id: String, future: Future[Unit]): Unit =
     {
       future.cancel()
       result(id, Scala.Tag.INTERRUPT, Nil)
     }
 
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
           def body: Unit =
           {
             val (tag, res) = Scala.function_body(name, msg.chunks)
             result(id, tag, res)
           }
           val future =
             if (Scala.function_thread(name)) {
               Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
             }
             else Future.fork(body)
           futures += (id -> future)
           true
         case _ => false
       }
     }
 
     private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
     {
       msg.properties match {
         case Markup.Cancel_Scala(id) =>
           futures.get(id) match {
             case Some(future) => cancel(id, future)
             case None =>
           }
           true
         case _ => false
       }
     }
 
     override val functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
   }
 }
 
 class Scala_Functions extends Scala.Functions(
   Scala.Echo,
   Scala.Sleep,
   Scala.Toplevel,
   Doc.Doc_Names,
   Bash.Process,
   Bibtex.Check_Database,
   Isabelle_System.Make_Directory,
   Isabelle_System.Copy_Dir,
   Isabelle_System.Copy_File,
   Isabelle_System.Copy_File_Base,
   Isabelle_System.Rm_Tree,
   Isabelle_System.Download,
   Isabelle_System.Isabelle_Id,
   Isabelle_Tool.Isabelle_Tools,
   isabelle.atp.SystemOnTPTP.List_Systems,
   isabelle.atp.SystemOnTPTP.Run_System)
diff --git a/src/Pure/library.scala b/src/Pure/library.scala
--- a/src/Pure/library.scala
+++ b/src/Pure/library.scala
@@ -1,303 +1,309 @@
 /*  Title:      Pure/library.scala
     Author:     Makarius
 
 Basic library.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object Library
 {
   /* resource management */
 
   def using[A <: AutoCloseable, B](a: A)(f: A => B): B =
   {
     try { f(a) }
     finally { if (a != null) a.close() }
   }
 
 
   /* integers */
 
   private val small_int = 10000
   private lazy val small_int_table =
   {
     val array = new Array[String](small_int)
     for (i <- 0 until small_int) array(i) = i.toString
     array
   }
 
   def is_small_int(s: String): Boolean =
   {
     val len = s.length
     1 <= len && len <= 4 &&
     s.forall(c => '0' <= c && c <= '9') &&
     (len == 1 || s(0) != '0')
   }
 
   def signed_string_of_long(i: Long): String =
     if (0 <= i && i < small_int) small_int_table(i.toInt)
     else i.toString
 
   def signed_string_of_int(i: Int): String =
     if (0 <= i && i < small_int) small_int_table(i)
     else i.toString
 
 
   /* separated chunks */
 
   def separate[A](s: A, list: List[A]): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     var first = true
     for (x <- list) {
       if (first) {
         first = false
         result += x
       }
       else {
         result += s
         result += x
       }
     }
     result.toList
   }
 
   def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] =
     new Iterator[CharSequence] {
       private val end = source.length
       private def next_chunk(i: Int): Option[(CharSequence, Int)] =
       {
         if (i < end) {
           var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
           Some((source.subSequence(i + 1, j), j))
         }
         else None
       }
       private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
 
       def hasNext: Boolean = state.isDefined
       def next(): CharSequence =
         state match {
           case Some((s, i)) => state = next_chunk(i); s
           case None => Iterator.empty.next()
         }
     }
 
   def space_explode(sep: Char, str: String): List[String] =
     separated_chunks(_ == sep, str).map(_.toString).toList
 
 
   /* lines */
 
   def terminate_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("", "\n", "\n")
 
   def cat_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
     if (str == "") str else cat_lines(split_lines(str).map(prfx + _))
 
   def first_line(source: CharSequence): String =
   {
     val lines = separated_chunks(_ == '\n', source)
     if (lines.hasNext) lines.next().toString
     else ""
   }
 
   def trim_line(s: String): String =
     if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
     else s
 
   def trim_split_lines(s: String): List[String] =
     split_lines(trim_line(s)).map(trim_line)
 
   def encode_lines(s: String): String = s.replace('\n', '\u000b')
   def decode_lines(s: String): String = s.replace('\u000b', '\n')
 
 
   /* strings */
 
   def cat_strings0(strs: IterableOnce[String]): String =
     strs.iterator.mkString("\u0000")
 
   def split_strings0(str: String): List[String] = space_explode('\u0000', str)
 
   def make_string(f: StringBuilder => Unit): String =
   {
     val s = new StringBuilder
     f(s)
     s.toString
   }
 
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
   def try_unsuffix(sffx: String, s: String): Option[String] =
     if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
 
   def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s
   def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s
 
   def isolate_substring(s: String): String = new String(s.toCharArray)
 
   def strip_ansi_color(s: String): String =
     s.replaceAll("\u001b\\[\\d+m", "")
 
 
   /* quote */
 
   def single_quote(s: String): String = "'" + s + "'"
 
   def quote(s: String): String = "\"" + s + "\""
 
   def try_unquote(s: String): Option[String] =
     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
     else None
 
   def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
 
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   {
     require(0 <= start && start <= end && end <= text.length, "bad reverse range")
 
     def this(text: CharSequence) = this(text, 0, text.length)
 
     def length: Int = end - start
     def charAt(i: Int): Char = text.charAt(end - i - 1)
 
     def subSequence(i: Int, j: Int): CharSequence =
       if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
       else throw new IndexOutOfBoundsException
 
     override def toString: String =
     {
       val buf = new StringBuilder(length)
       for (i <- 0 until length)
         buf.append(charAt(i))
       buf.toString
     }
   }
 
   class Line_Termination(text: CharSequence) extends CharSequence
   {
     def length: Int = text.length + 1
     def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
     def subSequence(i: Int, j: Int): CharSequence =
       if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
       else text.subSequence(i, j)
     override def toString: String = text.toString + "\n"
   }
 
 
   /* regular expressions */
 
   def make_regex(s: String): Option[Regex] =
     try { Some(new Regex(s)) } catch { case ERROR(_) => None }
 
   def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c)
 
   def escape_regex(s: String): String =
     if (s.exists(is_regex_meta)) {
       (for (c <- s.iterator)
        yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString
     }
     else s
 
 
   /* lists */
 
   def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
     (xs.takeWhile(pred), xs.dropWhile(pred))
 
   def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) =
   {
     val rev_xs = xs.reverse
     (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse)
   }
 
   def trim[A](pred: A => Boolean, xs: List[A]): List[A] =
     take_suffix(pred, take_prefix(pred, xs)._2)._1
 
   def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
 
   def merge[A](xs: List[A], ys: List[A]): List[A] =
     if (xs.eq(ys)) xs
     else if (xs.isEmpty) ys
     else ys.foldRight(xs)(Library.insert(_)(_))
 
   def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
     result.toList
   }
 
   def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>
           if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
           dups(xs)
       }
     dups(lst)
     result.toList
   }
 
   def replicate[A](n: Int, a: A): List[A] =
     if (n < 0) throw new IllegalArgumentException
     else if (n == 0) Nil
     else {
       val res = new mutable.ListBuffer[A]
       (1 to n).foreach(_ => res += a)
       res.toList
     }
 
+  def the_single[A](xs: List[A]): A =
+    xs match {
+      case List(x) => x
+      case _ => error("Single argument expected")
+    }
+
 
   /* proper values */
 
   def proper_string(s: String): Option[String] =
     if (s == null || s == "") None else Some(s)
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
 
 
   /* reflection */
 
   def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean =
   {
     import scala.language.existentials
     @tailrec def subclass(c: Class[_]): Boolean =
     {
       c == b ||
         {
           val d = c.getSuperclass
           d != null && subclass(d)
         }
     }
     subclass(a)
   }
 }