# HG changeset patch
# User wenzelm
# Date 1530049168 -7200
# Node ID 9d78b02b55060e37e4f77e7d0993d59a4d1a6a40
# Parent  e76c2d720701d27a425a14f9f834332057a8c5bf# Parent  e1c24b628ca5dffc52b51ed1b886f748ca917c4a
merged

diff -r e76c2d720701 -r 9d78b02b5506 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Jun 26 21:59:05 2018 +0100
+++ b/src/Pure/General/path.ML	Tue Jun 26 23:39:28 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;