src/Pure/library.scala
changeset 65715 e57e5935c6b4
parent 65712 ddd6dfc28e80
child 65718 79be5b464a16
--- 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 */