src/Pure/Thy/document_build.scala

--- a/src/Pure/Thy/document_build.scala	Wed Jun 14 11:18:25 2023 +0200
+++ b/src/Pure/Thy/document_build.scala	Wed Jun 14 11:47:43 2023 +0200
@@ -64,10 +64,9 @@
     val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =
-      SQL.where(
-        SQL.and(
-          Data.session_name.equal(session_name),
-          if_proper(name, Data.name.equal(name))))
+      SQL.where_and(
+        Data.session_name.equal(session_name),
+        if_proper(name, Data.name.equal(name)))
   }
 
   def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =