tuned;

--- a/src/Pure/Admin/afp.scala	Tue Apr 09 17:06:15 2019 +0200
+++ b/src/Pure/Admin/afp.scala	Wed Apr 10 12:11:30 2019 +0200
@@ -41,7 +41,7 @@
     def get(prop: String): Option[String] = Properties.get(metadata, prop)
     def get_string(prop: String): String = get(prop).getOrElse("")
     def get_strings(prop: String): List[String] =
-      Library.space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
+      space_explode(',', get_string(prop)).map(_.trim).filter(_.nonEmpty)
 
     def title: String = get_string("title")
     def authors: List[String] = get_strings("author")