1.1 --- a/src/Pure/General/path.ML	Sun Apr 22 11:05:04 2012 +0200
     1.2 +++ b/src/Pure/General/path.ML	Sun Apr 22 14:30:18 2012 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4  local
     1.5  
     1.6  fun explode_elem ".." = Parent
     1.7 -  | explode_elem "~" = Variable "HOME"
     1.8 +  | explode_elem "~" = Variable "USER_HOME"
     1.9    | explode_elem "~~" = Variable "ISABELLE_HOME"
    1.10    | explode_elem s =
    1.11        (case raw_explode s of