diff -r 186e07be32c3 -r a004c5322ea4 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jan 03 15:42:25 2023 +0100
+++ b/src/Pure/General/path.scala	Tue Jan 03 16:05:07 2023 +0100
@@ -293,26 +293,6 @@
   def file_name: String = expand.base.implode
 
 
-  /* implode wrt. given directories */
-
-  def implode_symbolic: String = {
-    val directories =
-      Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
-    val full_name = expand.implode
-    directories.view.flatMap(a =>
-      try {
-        val b = Path.explode(a).expand.implode
-        if (full_name == b) Some(a)
-        else {
-          Library.try_unprefix(b + "/", full_name) match {
-            case Some(name) => Some(a + "/" + name)
-            case None => None
-          }
-        }
-      } catch { case ERROR(_) => None }).headOption.getOrElse(implode)
-  }
-
-
   /* platform files */
 
   def file: JFile = File.platform_file(this)