src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Wed May 03 16:01:01 2017 +0200
+++ b/src/Pure/General/sql.scala	Wed May 03 16:15:09 2017 +0200
@@ -103,12 +103,12 @@
 
     def ident: String = SQL.ident(name)
 
-    def sql_decl(sql_type: Type.Value => String): String =
+    def decl(sql_type: Type.Value => String): String =
       ident + " " + sql_type(T) + (if (strict || primary_key) " NOT NULL" else "")
 
     def where_equal(s: String): String = "WHERE " + ident + " = " + string(s)
 
-    override def toString: String = sql_decl(sql_type_default)
+    override def toString: String = ident
   }
 
 
@@ -130,20 +130,17 @@
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
-    def sql_columns(sql_type: Type.Value => String): String =
+    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
     {
       val primary_key =
         columns.filter(_.primary_key).map(_.name) match {
           case Nil => Nil
           case keys => List("PRIMARY KEY " + enclosure(keys))
         }
-      enclosure(columns.map(_.sql_decl(sql_type)) ::: primary_key)
+      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
+        ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
     }
 
-    def create(strict: Boolean = false, sql_type: Type.Value => String): String =
-      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
-        ident + " " + sql_columns(sql_type)
-
     def create_index(index_name: String, index_columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): String =
       "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
@@ -162,8 +159,7 @@
       SQL.select(select_columns, distinct = distinct) + ident +
         (if (sql == "") "" else " " + sql)
 
-    override def toString: String =
-      "TABLE " + ident + " " + sql_columns(sql_type_default)
+    override def toString: String = ident
   }