# HG changeset patch
# User wenzelm
# Date 1530047748 -7200
# Node ID e1c24b628ca5dffc52b51ed1b886f748ca917c4a
# Parent  0854edc4d415b4fad6d8751cafa74702fa79e71f
smart_implode "$AFP" as well;

diff -r 0854edc4d415 -r e1c24b628ca5 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Jun 26 19:29:14 2018 +0200
+++ b/src/Pure/General/path.ML	Tue Jun 26 23:15:48 2018 +0200
@@ -214,15 +214,16 @@
   let
     val full_name = implode_path (expand path);
     fun fold_path a =
-      let val b = implode_path (expand (explode_path a)) in
-        if full_name = b then SOME a
-        else
-          (case try (unprefix (b ^ "/")) full_name of
-            SOME name => SOME (a ^ "/" ^ name)
-          | NONE => NONE)
-      end;
+      (case try (implode_path o expand o explode_path) a of
+        SOME b =>
+          if full_name = b then SOME a
+          else
+            (case try (unprefix (b ^ "/")) full_name of
+              SOME name => SOME (a ^ "/" ^ name)
+            | NONE => NONE)
+      | NONE => NONE);
   in
-    (case get_first fold_path ["~~", "$ISABELLE_HOME_USER", "~"] of
+    (case get_first fold_path ["$AFP", "~~", "$ISABELLE_HOME_USER", "~"] of
       SOME name => name
     | NONE => implode_path path)
   end;