src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Thu Nov 22 15:47:58 2018 +0100
+++ b/src/Pure/General/sql.scala	Thu Nov 22 17:34:30 2018 +0100
@@ -36,7 +36,7 @@
     }
 
   def string(s: String): Source =
-    "'" + s.map(escape_char(_)).mkString + "'"
+    s.iterator.map(escape_char(_)).mkString("'", "", "'")
 
   def ident(s: String): Source =
     Long_Name.implode(Long_Name.explode(s).map(a => quote(a.replace("\"", "\"\""))))