unused (amending 3d723062dc70);
authorwenzelm
Thu, 25 Aug 2022 11:29:55 +0200
changeset 75965 fe686d96d7ff
parent 75964 fd9734380709
child 75966 ed29a23e8b62
unused (amending 3d723062dc70);
src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Aug 25 11:24:13 2022 +0200
+++ b/src/Pure/General/sql.scala	Thu Aug 25 11:29:55 2022 +0200
@@ -131,9 +131,6 @@
   /* tables */
 
   sealed case class Table(name: String, columns: List[Column], body: Source = "") {
-    private val columns_index: Map[String, Int] =
-      columns.iterator.map(_.name).zipWithIndex.toMap
-
     Library.duplicates(columns.map(_.name)) match {
       case Nil =>
       case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))