# HG changeset patch
# User wenzelm
# Date 1661419795 -7200
# Node ID fe686d96d7ff7625228cc81b2468343d8cb1620f
# Parent  fd9734380709d0d063f462f288641390a75ae028
unused (amending 3d723062dc70);

diff -r fd9734380709 -r fe686d96d7ff 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))