tuned;

--- a/src/Pure/Thy/export.scala	Sun Aug 20 22:24:24 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Aug 21 10:53:26 2023 +0200
@@ -272,19 +272,16 @@
                   val buffer = new mutable.ListBuffer[Option[Entry]]
 
                   for ((entry, strict) <- args) {
-                    if (progress.stopped) {
+                    if (progress.stopped || known(entry.entry_name)) {
                       buffer += None
-                    }
-                    else if (known(entry.entry_name)) {
-                      if (strict) {
+                      if (strict && known(entry.entry_name)) {
                         val msg = message("Duplicate export", entry.theory_name, entry.name)
                         errors.change(msg :: _)
                       }
-                      buffer += None
                     }
                     else {
+                      buffer += Some(entry)
                       known += entry.entry_name
-                      buffer += Some(entry)
                     }
                   }