diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index 704034f5175c4e76df52431f205b3ab2956113e1..8028479f78cda9fe9a39590f33e7ae8faf2ac3d8 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -223,8 +223,8 @@ structure Resources' = struct
           SOME dir => dir
         | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
       val path = dir + Path.explode name handle ERROR msg => err msg;
-      val path' = Path.implode_symbolic path;
-      val _ = Path.expand path handle ERROR msg => err msg;
+      val path = Path.expand path handle ERROR msg => err msg;
+      val path' = Path.implode path;
       val _ = Context_Position.report ctxt pos (Markup.path path');
       val _ : Path.T = check_file path handle ERROR msg => err msg;
     in path' end;
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
index 4b48c444b7a2ddcd8fc58e0b98797dfc306136ff..59a009ae99bf424440af96de7d7964e5c9f69798 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
@@ -209,8 +209,8 @@ structure Resources' = struct
           SOME dir => dir
         | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
       val path = dir + Path.explode name handle ERROR msg => err msg;
-      val path' = Path.implode_symbolic path;
-      val _ = Path.expand path handle ERROR msg => err msg;
+      val path = Path.expand path handle ERROR msg => err msg;
+      val path' = Path.implode path;
       val _ = Context_Position.report ctxt pos (Markup.path path');
       val _ : Path.T = check_file path handle ERROR msg => err msg;
     in path' end;