src/Pure/General/sql.scala
changeset 79861 47705d905420
parent 79860 c49cb2a1ec44
child 79882 6f9ae0f052bc
--- a/src/Pure/General/sql.scala	Mon Mar 11 20:33:49 2024 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:44:34 2024 +0100
@@ -142,6 +142,8 @@
     primary_key: Boolean = false,
     expr: SQL.Source = ""
   ) {
+    def equals_name(other: Column): Boolean = name == other.name
+
     def make_primary_key: Column = copy(primary_key = true)
 
     def apply(table: Table): Column =