diff -r 7693ba6d65bc -r e57e5935c6b4 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu May 04 12:27:18 2017 +0200
+++ b/src/Pure/library.scala	Thu May 04 12:30:19 2017 +0200
@@ -147,9 +147,6 @@
   def proper_string(s: String): Option[String] =
     if (s == "") None else Some(s)
 
-  def proper_string_default(s: String, default: => String): String =
-    if (s == "") default else s
-
 
   /* quote */