diff --git a/Admin/Isabelle_app/build b/Admin/Isabelle_app/build
--- a/Admin/Isabelle_app/build
+++ b/Admin/Isabelle_app/build
@@ -1,15 +1,16 @@
 #!/usr/bin/env bash
 
 set -e
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 cd "$THIS"
 
 source "../../lib/scripts/isabelle-platform"
 
 PLATFORM="${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}"
 mkdir -p "$PLATFORM"
 
 EXE="$PLATFORM/Isabelle"
 gcc -Wall Isabelle.c -o "$EXE"
 echo "$EXE"
diff --git a/Admin/bash_process/build b/Admin/bash_process/build
--- a/Admin/bash_process/build
+++ b/Admin/bash_process/build
@@ -1,51 +1,52 @@
 #!/usr/bin/env bash
 #
 # Multi-platform build script
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 PRG="$(basename "$0")"
 
 
 # diagnostics
 
 function usage()
 {
   echo
   echo "Usage: $PRG TARGET"
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 # command line args
 
 [ "$#" -eq 0 ] && usage
 TARGET="$1"; shift
 
 [ "$#" -eq 0 ] || usage
 
 
 # main
 
 mkdir -p "$TARGET"
 
 case "$TARGET" in
   arm64-linux)
     cc -Wall bash_process.c -o "$TARGET/bash_process"
     ;;
   x86_64-linux | x86_64-darwin)
     cc -Wall -m64 bash_process.c -o "$TARGET/bash_process"
     ;;
   x86_64-cygwin)
     cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
     ;;
   *)
     fail "Bad target platform: \"$TARGET\""
     ;;
 esac
diff --git a/Admin/build b/Admin/build
--- a/Admin/build
+++ b/Admin/build
@@ -1,90 +1,91 @@
 #!/usr/bin/env bash
 #
 # Administrative build for Isabelle source distribution.
 
 ## directory layout
 
 if [ -z "$ISABELLE_HOME" ]; then
+  unset CDPATH
   ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
   ISABELLE_TOOL="$ISABELLE_HOME/bin/isabelle"
 fi
 
 
 ## diagnostics
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   cat <<EOF
 
 Usage: $PRG [MODULES]
 
   Produce Isabelle distribution modules from current repository sources.
   The MODULES list may contain any of the following:
 
     all             all modules below
     browser         graph browser
     jars            Isabelle/Scala
     jars_fresh      fresh build of jars
 
 EOF
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 [ "$#" -eq 0 ] && usage
 
 MODULES="$@"; shift "$#"
 
 
 ## modules
 
 function build_all ()
 {
   build_browser
   build_jars
 }
 
 
 function build_browser ()
 {
   pushd "$ISABELLE_HOME/lib/browser" >/dev/null
   "$ISABELLE_TOOL" env ./build || exit $?
   popd >/dev/null
 }
 
 
 function build_jars ()
 {
   pushd "$ISABELLE_HOME" >/dev/null
   "$ISABELLE_TOOL" env src/Pure/build-jars "$@" || exit $?
   popd >/dev/null
 }
 
 
 ## main
 
 #FIXME workarounds for scalac 2.11.0
 export CYGWIN="nodosfilewarning"
 function stty() { :; }
 export -f stty
 
 for MODULE in $MODULES
 do
   case $MODULE in
     all) build_all;;
     browser) build_browser;;
     jars) build_jars;;
     jars_fresh) build_jars -f;;
     *) fail "Bad module $MODULE"
   esac
 done
diff --git a/Admin/build_history b/Admin/build_history
--- a/Admin/build_history
+++ b/Admin/build_history
@@ -1,8 +1,9 @@
 #!/usr/bin/env bash
 #
 # DESCRIPTION: build history versions from another repository clone
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
 "$THIS/build" jars > /dev/null || exit $?
 exec "$THIS/../bin/isabelle_java" isabelle.Build_History "$@"
diff --git a/Admin/build_release b/Admin/build_release
--- a/Admin/build_release
+++ b/Admin/build_release
@@ -1,8 +1,9 @@
 #!/usr/bin/env bash
 #
 # DESCRIPTION: build full Isabelle distribution from repository
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
 "$THIS/build" jars || exit $?
 exec "$THIS/../bin/isabelle_java" isabelle.Build_Release "$@"
diff --git a/Admin/cronjob/main b/Admin/cronjob/main
--- a/Admin/cronjob/main
+++ b/Admin/cronjob/main
@@ -1,12 +1,13 @@
 #!/usr/bin/env bash
 #
 # DESCRIPTION: start the main Isabelle cronjob
 
+unset CDPATH
 THIS="$(cd "$(dirname "$0")"; pwd)"
 
 source "$HOME/.bashrc"
 
 export ISABELLE_IDENTIFIER="cronjob"
 "$THIS/../build" jars_fresh || exit $?
 
 exec "$THIS/../../bin/isabelle_java" isabelle.Isabelle_Cronjob "$@"
diff --git a/Admin/init b/Admin/init
--- a/Admin/init
+++ b/Admin/init
@@ -1,205 +1,206 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # DESCRIPTION: initialize Isabelle repository clone or repository archive
 
 
 ## environment
 
+unset CDPATH
 export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 
 ISABELLE_REPOS="https://isabelle.sketis.net/repos/isabelle"
 
 
 ## diagnostics
 
 function usage()
 {
   echo
   echo "Usage: Admin/init [OPTIONS]"
   echo
   echo "  Options are:"
   echo "    -C           force clean working directory (no backup!)"
   echo "    -I NAME      set \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER (or reset via -I:)"
   echo "    -L           local history only: no pull from repository server"
   echo "    -R           version is current official release"
   echo "    -U URL       Isabelle repository server"
   echo "                 (default: \"$ISABELLE_REPOS\")"
   echo "    -V PATH      version is taken from file, or directory"
   echo "                 with file \"ISABELLE_VERSION\""
   echo "    -c           check clean working directory"
   echo "    -f           fresh build of Isabelle/Scala/jEdit"
   echo "    -n           no build of Isabelle/Scala/jEdit"
   echo "    -r REV       version given in Mercurial notation (changeset id or tag)"
   echo "    -u           update to latest tip"
   echo
   echo "  Initialize the current ISABELLE_HOME directory, which needs to be a"
   echo "  repository clone (all versions) or repository archive (fixed version)."
   echo "  Download required components. Build Isabelle/Scala/jEdit by default."
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 #options
 
 BUILD_OPTIONS="-b"
 UPDATE_IDENTIFIER=""
 IDENTIFIER=""
 PULL="true"
 
 CLEAN_FORCE=""
 CLEAN_CHECK=""
 
 VERSION=""
 VERSION_RELEASE=""
 VERSION_PATH=""
 VERSION_REV=""
 
 while getopts "CI:LRU:V:cfnr:u" OPT
 do
   case "$OPT" in
     C)
       CLEAN_FORCE="--clean"
       ;;
     I)
       UPDATE_IDENTIFIER="true"
       if [ "$OPTARG" = ":" ]; then
         IDENTIFIER=""
       else
         IDENTIFIER="$OPTARG"
       fi
       ;;
     L)
       PULL=""
       ;;
     R)
       VERSION="true"
       VERSION_RELEASE="true"
       VERSION_PATH=""
       VERSION_REV=""
       ;;
     U)
       ISABELLE_REPOS="$OPTARG"
       ;;
     V)
       VERSION="true"
       VERSION_RELEASE=""
       VERSION_PATH="$OPTARG"
       VERSION_REV=""
       ;;
     c)
       CLEAN_CHECK="--check"
       ;;
     f)
       BUILD_OPTIONS="-b -f"
       ;;
     n)
       BUILD_OPTIONS=""
       ;;
     r)
       VERSION="true"
       VERSION_RELEASE=""
       VERSION_PATH=""
       VERSION_REV="$OPTARG"
       ;;
     u)
       VERSION="true"
       VERSION_RELEASE=""
       VERSION_PATH=""
       VERSION_REV="tip"
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -ne 0 ] && usage
 
 
 ## main
 
 if [ -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER" ]; then
   OLD_IDENTIFIER="$(cat "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER")"
 else
   OLD_IDENTIFIER=""
 fi
 
 if [ -n "$UPDATE_IDENTIFIER" -a "$IDENTIFIER" != "$OLD_IDENTIFIER" ]; then
   OLD_ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
   if [ -n "$IDENTIFIER" ]; then
     echo -n "$IDENTIFIER" > "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
   else
     rm -f "$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER"
   fi
   ISABELLE_HOME_USER="$("$ISABELLE_HOME/bin/isabelle" getenv -b ISABELLE_HOME_USER)"
   echo "Changed \$ISABELLE_HOME/etc/ISABELLE_IDENTIFIER: \"$OLD_IDENTIFIER\" ~> \"$IDENTIFIER\""
   echo "Changed \$ISABELLE_HOME_USER: \"$OLD_ISABELLE_HOME_USER\" ~> \"$ISABELLE_HOME_USER\""
 fi
 
 if [ -z "$VERSION" ]; then
   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
   "$ISABELLE_HOME/bin/isabelle" components -a || exit "$?"
   if [ -n "$BUILD_OPTIONS" ]; then
     "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
   fi
 elif [ ! -d "$ISABELLE_HOME/.hg" ]; then
   fail "Not a repository clone: cannot switch version"
 else
   if [ -n "$VERSION_REV" ]; then
     REV="$VERSION_REV"
   elif [ -n "$VERSION_RELEASE" ]; then
     URL="$ISABELLE_REPOS/raw-file/tip/Admin/Release/official"
     REV="$(curl -s -f "$URL" | head -n1)"
     [ -z "$REV" ] && fail "Failed to access \"$URL\""
   elif [ -f "$VERSION_PATH" ]; then
     REV="$(cat "$VERSION_PATH")"
   elif [ -d "$VERSION_PATH" ]; then
     if [ -f "$VERSION_PATH/ISABELLE_VERSION" ]; then
       REV="$(cat "$VERSION_PATH/ISABELLE_VERSION")"
     else
       fail "Missing file \"$VERSION_PATH/ISABELLE_VERSION\""
     fi
   else
     fail "Missing file \"$VERSION_PATH\""
   fi
 
   "$ISABELLE_HOME/bin/isabelle" components -I || exit "$?"
 
   export LANG=C
   export HGPLAIN=
 
   #Atomic exec: avoid inplace update of running script!
   export PULL CLEAN_FORCE CLEAN_CHECK REV ISABELLE_REPOS BUILD_OPTIONS
   exec bash -c '
     set -e
     if [ -n "$PULL" ]; then
       "${HG:-hg}" -R "$ISABELLE_HOME" pull -r "$REV" "$ISABELLE_REPOS"
     fi
     "${HG:-hg}" -R "$ISABELLE_HOME" update -r "$REV" $CLEAN_FORCE $CLEAN_CHECK
     "$ISABELLE_HOME/bin/isabelle" components -a
     if [ -n "$BUILD_OPTIONS" ]; then
       "$ISABELLE_HOME/bin/isabelle" jedit $BUILD_OPTIONS
     fi
     "${HG:-hg}" -R "$ISABELLE_HOME" log -r "$REV"
     if [ ! -f "$ISABELLE_HOME/Admin/init" ]; then
       echo >&2 "### The Admin/init script has disappeared in this version"
       echo >&2 "### (need to invoke \"${HG:-hg} update\" before using it again)"
     fi
   '
 fi
diff --git a/bin/isabelle b/bin/isabelle
--- a/bin/isabelle
+++ b/bin/isabelle
@@ -1,49 +1,51 @@
 #!/usr/bin/env bash
 #
 # Author: Markus Wenzel, TU Muenchen
 #
 # Isabelle tool wrapper.
 
+unset CDPATH
+
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
 ## settings
 
 PRG="$(basename "$0")"
 
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## external tool (shell script)
 
 if [ "$#" -ge 1 -a "$1" != "-?" ]
 then
   TOOL_NAME="$1"
 
   splitarray ":" "$ISABELLE_TOOLS"; TOOLS=("${SPLITARRAY[@]}")
   for DIR in "${TOOLS[@]}"
   do
     TOOL="$DIR/$TOOL_NAME"
     case "$TOOL" in
       *~ | *.orig) ;;
       *)
         if [ -f "$TOOL" -a -x "$TOOL" ]; then
           shift
           exec "$TOOL" "$@"
         fi
         ;;
     esac
   done
 fi
 
 
 ## internal tool or usage (Scala)
 
 isabelle_admin_build jars || exit $?
 
 eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
 exec isabelle java "${JAVA_ARGS[@]}" isabelle.Isabelle_Tool "$@"
diff --git a/bin/isabelle_java b/bin/isabelle_java
--- a/bin/isabelle_java
+++ b/bin/isabelle_java
@@ -1,72 +1,74 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # Isabelle/Java cold start -- without settings environment
 
+unset CDPATH
+
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 export ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 
 (
   source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
   eval "declare -a JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS $ISABELLE_TOOL_JAVA_OPTIONS)"
 
   if [ -f "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar" ]; then
     classpath "$ISABELLE_HOME/src/Tools/jEdit/dist/jedit.jar"
   fi
 
   [ -n "$CLASSPATH" ] && classpath "$CLASSPATH"
 
   echo "$ISABELLE_ROOT"
   echo "$CYGWIN_ROOT"
   echo "$JAVA_HOME"
   echo "$(platform_path "$ISABELLE_CLASSPATH")"
   for ARG in "${JAVA_ARGS[@]}"; do echo "$ARG"; done
 ) | {
   LINE_COUNT=0
   export ISABELLE_ROOT=""
   export CYGWIN_ROOT=""
   unset JAVA_HOME
   unset ISABELLE_CLASSPATH
   unset JAVA_ARGS; declare -a JAVA_ARGS
 
   while { unset REPLY; read -r; test "$?" = 0 -o -n "$REPLY"; }
   do
     case "$LINE_COUNT" in
       0)
         LINE_COUNT=1
         ISABELLE_ROOT="$REPLY"
         ;;
       1)
         LINE_COUNT=2
         CYGWIN_ROOT="$REPLY"
         ;;
       2)
         LINE_COUNT=3
         JAVA_HOME="$REPLY"
         ;;
       3)
         LINE_COUNT=4
         ISABELLE_CLASSPATH="$REPLY"
         ;;
       *)
         JAVA_ARGS["${#JAVA_ARGS[@]}"]="$REPLY"
         ;;
     esac
   done
 
   if [ -z "$JAVA_HOME" ]; then
     echo "Unknown JAVA_HOME -- Java unavailable" >&2
     exit 127
   else
     unset ISABELLE_HOME
     unset CLASSPATH
     exec "$JAVA_HOME/bin/java" "${JAVA_ARGS[@]}" \
       -classpath "$ISABELLE_CLASSPATH" "$@"
   fi
 }
diff --git a/bin/isabelle_scala_script b/bin/isabelle_scala_script
--- a/bin/isabelle_scala_script
+++ b/bin/isabelle_scala_script
@@ -1,24 +1,26 @@
 #!/usr/bin/env bash
 #
 # Author: Makarius
 #
 # Isabelle/Scala script wrapper.
 
+unset CDPATH
+
 if [ -L "$0" ]; then
   TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
   exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
 fi
 
 
 ## settings
 
 PRG="$(basename "$0")"
 
 ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
 
 
 ## main
 
 exec "$ISABELLE_TOOL" scala -howtorun:script -nocompdaemon "$@"
 
diff --git a/src/Tools/Metis/fix_metis_license b/src/Tools/Metis/fix_metis_license
--- a/src/Tools/Metis/fix_metis_license
+++ b/src/Tools/Metis/fix_metis_license
@@ -1,4 +1,5 @@
 #!/usr/bin/env bash
+unset CDPATH
 THIS=$(cd "$(dirname "$0")"; echo $PWD)
 (cd $THIS;
  perl -p -i~ -w -e 's/MIT license/BSD License/g' Makefile src/*.s* scripts/mlpp)
diff --git a/src/Tools/Metis/make_metis b/src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis
+++ b/src/Tools/Metis/make_metis
@@ -1,54 +1,55 @@
 #!/usr/bin/env bash
 #
 # make_metis - turn original Metis files into Isabelle ML source.
 #
 # Signatures, structures, and functors are renamed to have a "Metis_" prefix.
 # A few other ad hoc transformations are performed to ensure that the sources
 # compile within Isabelle on Poly/ML and SML/NJ.
 
+unset CDPATH
 THIS=$(cd "$(dirname "$0")"; echo $PWD)
 make -f Makefile.FILES refresh_FILES
 FILES=$(cat "$THIS/FILES")
 
 (
   cat <<EOF
 (*
    This file was generated by the "make_metis" script. The BSD License is used
    with Joe Leslie-Hurd's kind permission. Extract from a September 13, 2010
    email written by him:
 
        I hereby give permission to the Isabelle team to release Metis as part
        of Isabelle, with the Metis code covered under the Isabelle BSD
        license.
 *)
 
 (******************************************************************)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (******************************************************************)
 
 EOF
 
   for FILE in $FILES
   do
     echo
     echo "(**** Original file: $FILE ****)"
     echo
     echo -e "$FILE" >&2
     "$THIS/scripts/mlpp" -c polyml "$FILE" | \
     perl -p -e \
 's/\bref\b/Unsynchronized.ref/g;'\
 "`grep "^\(signature\|structure\|functor\)" $FILES | \
   sed "s/[^:]*:[a-z]* \([A-Za-z0-9_]*\).*/\1/" | \
   tr " " "\n" | \
   sort | \
   uniq | \
   sed 's/\(.*\)/s\/\\\\b\1\\\\b\/Metis_\1\/g;/'`"
   done
 
   cat <<EOF
 ;
 EOF
 
 ) > metis.ML