# HG changeset patch
# User wenzelm
# Date 1686857191 -7200
# Node ID 1b97502461a39108aaa015fdb2fb1d8c6db50981
# Parent  70041580b81e813d16e944849f76761c4dfbe997
obsolete;

diff -r 70041580b81e -r 1b97502461a3 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu Jun 15 21:26:21 2023 +0200
+++ b/src/Pure/General/sql.scala	Thu Jun 15 21:26:31 2023 +0200
@@ -240,12 +240,6 @@
     def iterator: Iterator[Table] = list.iterator
 
     // requires transaction
-    def create_lock(db: Database): Unit = {
-      foreach(db.create_table(_))
-      lock(db)
-    }
-
-    // requires transaction
     def lock(db: Database, create: Boolean = false): Unit = {
       if (create) foreach(db.create_table(_))
       val sql = db.lock_tables(list)