diff -r cbd053fff24c -r 6c6797395a3a src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Fri Feb 24 11:07:31 2023 +0100
+++ b/src/Pure/General/sql.scala	Fri Feb 24 11:38:43 2023 +0100
@@ -55,10 +55,9 @@
   val join_inner: Source = " INNER JOIN "
   def join(outer: Boolean): Source = if (outer) join_outer else join_inner
 
-  def member(x: Source, set: Iterable[String]): Source = {
-    require(set.nonEmpty)
-    set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
-  }
+  def member(x: Source, set: Iterable[String]): Source =
+    if (set.isEmpty) "FALSE"
+    else set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
 
   def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)