eliminated redundant type SQL.View;
eliminated unused DROP operations;

--- a/src/Pure/Admin/build_log.scala	Tue May 02 21:57:32 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue May 02 23:21:53 2017 +0200
@@ -897,17 +897,21 @@
     /* full view on build_log data */
 
     // WARNING: This may cause performance problems, e.g. with sqlitebrowser
-    val full_view: SQL.View =
-      SQL.View("isabelle_build_log",
+    val full_view: SQL.Table =
+    {
+      val columns =
         Meta_Info.table.columns :::
-          Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false)),
-        {
-          val table1 = Meta_Info.table
-          val table2 = Build_Info.sessions_table
-          SQL.select(Meta_Info.log_name(table1) :: full_view.columns.tail) +
-          SQL.join(table1, table2,
-            Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql)
-        })
+          Build_Info.sessions_table.columns.tail.map(_.copy(primary_key = false))
+      SQL.Table("isabelle_build_log", columns,
+        view =
+          {
+            val table1 = Meta_Info.table
+            val table2 = Build_Info.sessions_table
+            SQL.select(Meta_Info.log_name(table1) :: columns.tail) +
+            SQL.join(table1, table2,
+              Meta_Info.log_name(table1).sql + " = " + Meta_Info.log_name(table2).sql)
+          })
+    }
 
 
     /* main operations */

--- a/src/Pure/General/sql.scala	Tue May 02 21:57:32 2017 +0200
+++ b/src/Pure/General/sql.scala	Tue May 02 23:21:53 2017 +0200
@@ -77,11 +77,6 @@
 
   /* columns */
 
-  trait Qualifier
-  {
-    def name: String
-  }
-
   object Column
   {
     def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column =
@@ -103,8 +98,8 @@
   sealed case class Column(
     name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false)
   {
-    def apply(qual: Qualifier): Column =
-      Column(Long_Name.qualify(qual.name, name), T, strict = strict, primary_key = primary_key)
+    def apply(table: Table): Column =
+      Column(Long_Name.qualify(table.name, name), T, strict = strict, primary_key = primary_key)
 
     def sql: String = identifer(name)
     def sql_decl(sql_type: Type.Value => String): String =
@@ -119,7 +114,7 @@
 
   /* tables */
 
-  sealed case class Table(name: String, columns: List[Column]) extends Qualifier
+  sealed case class Table(name: String, columns: List[Column], view: String = "")
   {
     private val columns_index: Map[String, Int] =
       columns.iterator.map(_.name).zipWithIndex.toMap
@@ -129,6 +124,8 @@
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
     }
 
+    def is_view: Boolean = view != ""
+
     def sql: String = identifer(name)
 
     def sql_columns(sql_type: Type.Value => String): String =
@@ -145,9 +142,6 @@
       "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
         identifer(name) + " " + sql_columns(sql_type)
 
-    def sql_drop(strict: Boolean): String =
-      "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + identifer(name)
-
     def sql_create_index(
         index_name: String, index_columns: List[Column],
         strict: Boolean, unique: Boolean): String =
@@ -155,9 +149,6 @@
         (if (strict) "" else "IF NOT EXISTS ") + identifer(index_name) + " ON " +
         identifer(name) + " " + enclosure(index_columns.map(_.name))
 
-    def sql_drop_index(index_name: String, strict: Boolean): String =
-      "DROP INDEX " + (if (strict) "" else "IF EXISTS ") + identifer(index_name)
-
     def sql_insert: String =
       "INSERT INTO " + identifer(name) + " VALUES " + enclosure(columns.map(_ => "?"))
 
@@ -172,17 +163,6 @@
   }
 
 
-  /* views */
-
-  sealed case class View(name: String, columns: List[Column], query: String) extends Qualifier
-  {
-    def sql: String = identifer(name)
-    def sql_create: String = "CREATE VIEW " + identifer(name) + " AS " + query
-
-    override def toString: String =
-      "VIEW " + identifer(name) + " " + enclosure(columns.map(_.sql_decl(sql_type_default)))
-  }
-
 
   /** SQL database operations **/
 
@@ -320,20 +300,18 @@
       using(statement(table.sql_create(strict, sql_type) + (if (sql == "") "" else " " + sql)))(
         _.execute())
 
-    def drop_table(table: Table, strict: Boolean = false): Unit =
-      using(statement(table.sql_drop(strict)))(_.execute())
-
     def create_index(table: Table, name: String, columns: List[Column],
         strict: Boolean = false, unique: Boolean = false): Unit =
       using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
 
-    def drop_index(table: Table, name: String, strict: Boolean = false): Unit =
-      using(statement(table.sql_drop_index(name, strict)))(_.execute())
-
-    def create_view(view: View, strict: Boolean = false): Unit =
-      if (strict || !tables.contains(view.name)) {
-        using(statement(view.sql_create))(_.execute())
+    def create_view(table: Table, strict: Boolean = false): Unit =
+    {
+      require(table.is_view)
+      if (strict || !tables.contains(table.name)) {
+        val sql = "CREATE VIEW " + identifer(table.name) + " AS " + table.view
+        using(statement(sql))(_.execute())
       }
+    }
   }
 }