# HG changeset patch
# User wenzelm
# Date 1689676760 -7200
# Node ID e47233dbeab752cf3400b051f0834f9d7d75440e
# Parent  a84f8fca08339bb2f4b24a82e5ea6e3e92b9a1c7
removed unused "create_index": implicit index from primary_key is usually sufficient;

diff -r a84f8fca0833 -r e47233dbeab7 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Tue Jul 18 12:32:07 2023 +0200
+++ b/src/Pure/General/sql.scala	Tue Jul 18 12:39:20 2023 +0200
@@ -198,12 +198,6 @@
         ident + " " + enclosure(columns.map(_.decl(sql_type)) ::: primary_key)
     }
 
-    def create_index(index_name: String, index_columns: List[Column],
-        strict: Boolean = false, unique: Boolean = false): Source =
-      "CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
-        (if (strict) "" else "IF NOT EXISTS ") + SQL.ident(index_name) + " ON " +
-        ident + " " + enclosure(index_columns.map(_.name))
-
     def insert_cmd(cmd: Source = "INSERT", sql: Source = ""): Source =
       cmd + " INTO " + ident + " VALUES " + enclosure(columns.map(_ => "?")) + SQL.separate(sql)
 
@@ -556,10 +550,6 @@
       }
     }
 
-    def create_index(table: Table, name: String, columns: List[Column],
-        strict: Boolean = false, unique: Boolean = false): Unit =
-      execute_statement(table.create_index(name, columns, strict, unique))
-
     def create_view(table: Table, strict: Boolean = false): Unit = {
       if (strict || !exists_table(table)) {
         execute_statement("CREATE VIEW " + table + " AS " + { table.query; table.body })