# HG changeset patch
# User wenzelm
# Date 1672486291 -3600
# Node ID 83e3d4075f2c59ec66dabf11f720053295cba562
# Parent  81848d12aba313858da0d789ac5f38972260881f
tuned;

diff -r 81848d12aba3 -r 83e3d4075f2c src/Pure/Thy/file_format.scala
--- a/src/Pure/Thy/file_format.scala	Sat Dec 31 12:25:34 2022 +0100
+++ b/src/Pure/Thy/file_format.scala	Sat Dec 31 12:31:31 2022 +0100
@@ -80,12 +80,12 @@
     name: Document.Node.Name
   ): Option[Document.Node.Name] = {
     for {
-      thy <- Url.get_base_name(name.node)
+      theory <- Url.get_base_name(name.node)
       if detect(name.node) && theory_suffix.nonEmpty
     }
     yield {
-      val thy_node = resources.append(name.node, Path.explode(theory_suffix))
-      Document.Node.Name(thy_node, master_dir = name.master_dir, theory = thy)
+      val node = resources.append(name.node, Path.explode(theory_suffix))
+      Document.Node.Name(node, master_dir = name.master_dir, theory = theory)
     }
   }