diff -r d7cefedbca94 -r 0c44e3e9126f src/Pure/General/sqlite.scala
--- a/src/Pure/General/sqlite.scala	Wed Feb 08 21:06:47 2017 +0100
+++ b/src/Pure/General/sqlite.scala	Wed Feb 08 22:11:37 2017 +0100
@@ -7,13 +7,11 @@
 package isabelle
 
 
-import java.sql.{DriverManager, Connection, PreparedStatement}
+import java.sql.{DriverManager, Connection}
 
 
 object SQLite
 {
-  /** database connection **/
-
   def open_database(path: Path): Database =
   {
     val path0 = path.expand
@@ -23,57 +21,10 @@
     new Database(path0, connection)
   }
 
-  class Database private[SQLite](path: Path, val connection: Connection)
+  class Database private[SQLite](path: Path, val connection: Connection) extends SQL_Database
   {
     override def toString: String = path.toString
 
-    def close() { connection.close }
-
     def rebuild { using(statement("VACUUM"))(_.execute()) }
-
-    def transaction[A](body: => A): A =
-    {
-      val auto_commit = connection.getAutoCommit
-      val savepoint = connection.setSavepoint
-
-      try {
-        connection.setAutoCommit(false)
-        val result = body
-        connection.commit
-        result
-      }
-      catch { case exn: Throwable => connection.rollback(savepoint); throw exn }
-      finally { connection.setAutoCommit(auto_commit) }
-    }
-
-
-    /* statements */
-
-    def statement(sql: String): PreparedStatement = connection.prepareStatement(sql)
-
-    def insert_statement(table: SQL.Table): PreparedStatement = statement(table.sql_insert)
-
-    def select_statement(table: SQL.Table, columns: List[SQL.Column[Any]],
-        sql: String = "", distinct: Boolean = false): PreparedStatement =
-      statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql))
-
-
-    /* tables */
-
-    def tables: List[String] =
-      SQL.iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList
-
-    def create_table(table: SQL.Table, strict: Boolean = true, rowid: Boolean = true): Unit =
-      using(statement(table.sql_create(strict, rowid)))(_.execute())
-
-    def drop_table(table: SQL.Table, strict: Boolean = true): Unit =
-      using(statement(table.sql_drop(strict)))(_.execute())
-
-    def create_index(table: SQL.Table, name: String, columns: List[SQL.Column[Any]],
-        strict: Boolean = true, unique: Boolean = false): Unit =
-      using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute())
-
-    def drop_index(table: SQL.Table, name: String, strict: Boolean = true): Unit =
-      using(statement(table.sql_drop_index(name, strict)))(_.execute())
   }
 }