diff -r 15f55d02ba67 -r a6d079e0575d src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Sat Aug 19 14:45:57 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Aug 19 22:57:06 2023 +0200
@@ -317,11 +317,14 @@
 
     def execute(): Boolean = rep.execute()
 
-    def execute_batch(batch: Statement => IterableOnce[Unit]): Unit = {
-      for (() <- batch(this).iterator) rep.addBatch()
-      val res = rep.executeBatch()
-      if (!res.forall(i => i >= 0 || i == java.sql.Statement.SUCCESS_NO_INFO)) {
-        throw new Batch_Error(res.toList)
+    def execute_batch(batch: Statement => IterableOnce[Boolean]): Unit = {
+      var proper = false
+      for (ok <- batch(this).iterator if ok) { rep.addBatch(); proper = true }
+      if (proper) {
+        val res = rep.executeBatch()
+        if (!res.forall(i => i >= 0 || i == java.sql.Statement.SUCCESS_NO_INFO)) {
+          throw new Batch_Error(res.toList)
+        }
       }
     }
 
@@ -511,7 +514,7 @@
 
     def execute_batch_statement(
       sql: Source,
-      batch: Statement => IterableOnce[Unit] = _ => Nil
+      batch: Statement => IterableOnce[Boolean] = _ => Nil
     ): Unit = using_statement(sql) { stmt => stmt.execute_batch(batch) }
 
     def execute_query_statement[A, B](