# HG changeset patch
# User wenzelm
# Date 1493663202 -7200
# Node ID 546020a98a919d7d02f40c41c3c3a2d325fc11ed
# Parent  490649872accf6ad46dba4d35f6fb4ed1de18e05
clarified treatment of qualified names (amending 7ef438495a02);

diff -r 490649872acc -r 546020a98a91 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon May 01 20:14:50 2017 +0200
+++ b/src/Pure/General/sql.scala	Mon May 01 20:26:42 2017 +0200
@@ -34,8 +34,7 @@
     "'" + s.map(escape_char(_)).mkString + "'"
 
   def ident(s: String): String =
-    if (Long_Name.is_qualified(s)) s
-    else quote(s.replace("\"", "\"\""))
+    Long_Name.implode(Long_Name.explode(s).map(_.replace("\"", "\"\"")))
 
   def enclose(s: String): String = "(" + s + ")"
   def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")