changeset 76843 | 3dfc89c8dd71 |
parent 76842 | 18465808e61f |
child 76846 | 83e3d4075f2c |
--- a/src/Pure/Thy/file_format.scala Sat Dec 31 11:58:45 2022 +0100 +++ b/src/Pure/Thy/file_format.scala Sat Dec 31 12:10:14 2022 +0100 @@ -85,7 +85,7 @@ } yield { val thy_node = resources.append(name.node, Path.explode(theory_suffix)) - Document.Node.Name(thy_node, name.master_dir, thy) + Document.Node.Name(thy_node, master_dir = name.master_dir, theory = thy) } }