src/Pure/General/sql.scala

--- a/src/Pure/General/sql.scala	Sat Mar 09 20:20:13 2024 +0100
+++ b/src/Pure/General/sql.scala	Sat Mar 09 20:52:06 2024 +0100
@@ -234,6 +234,11 @@
 
     def iterator: Iterator[Table] = list.iterator
 
+    def index(table: Table): Int =
+      iterator.zipWithIndex
+        .collectFirst({ case (t, i) if t.name == table.name => i })
+        .getOrElse(error("No table " + quote(table.name)))
+
     // requires transaction
     def lock(db: Database, create: Boolean = false): Boolean = {
       if (create) foreach(db.create_table(_))