src/Pure/library.scala

--- a/src/Pure/library.scala	Thu Jun 06 22:34:24 2024 +0200
+++ b/src/Pure/library.scala	Thu Jun 06 22:26:40 2024 +0200
@@ -285,42 +285,6 @@
     }
 
 
-  /* data update */
-
-  object Update {
-    sealed abstract class Op[A]
-    case class Delete[A](name: String) extends Op[A]
-    case class Insert[A](item: A) extends Op[A]
-
-    def data[A <: Name.T](old_data: Name.Data[A], updates: List[Op[A]]): Name.Data[A] =
-      updates.foldLeft(old_data) {
-        case (map, Delete(name)) => map - name
-        case (map, Insert(item)) => map + (item.name -> item)
-      }
-
-    val empty: Update = Update()
-
-    def make[A](a: Name.Data[A], b: Name.Data[A], kind: Int = 0): Update =
-      if (a eq b) empty
-      else {
-        val delete = List.from(for ((x, y) <- a.iterator if !b.get(x).contains(y)) yield x)
-        val insert = List.from(for ((x, y) <- b.iterator if !a.get(x).contains(y)) yield x)
-        Update(delete = delete, insert = insert, kind = kind)
-      }
-  }
-
-  sealed case class Update(
-    delete: List[String] = Nil,
-    insert: List[String] = Nil,
-    kind: Int = 0
-  ) {
-    def deletes: Boolean = delete.nonEmpty
-    def inserts: Boolean = insert.nonEmpty
-    def defined: Boolean = deletes || inserts
-    lazy val domain: Set[String] = delete.toSet ++ insert
-  }
-
-
   /* proper values */
 
   def proper_bool(b: Boolean): Option[Boolean] =