diff --git a/lib/Tools/version b/lib/Tools/version
--- a/lib/Tools/version
+++ b/lib/Tools/version
@@ -1,93 +1,95 @@
 #!/usr/bin/env bash
 #
 # Author: Stefan Berghofer, TU Muenchen
 # Author: Makarius
 #
 # DESCRIPTION: display Isabelle version
 
 
 PRG="$(basename "$0")"
 
 function usage()
 {
   echo
   echo "Usage: isabelle $PRG [OPTIONS]"
   echo
   echo "  Options are:"
   echo "    -i           short identification (derived from Mercurial id)"
   echo "    -t           symbolic tags (derived from Mercurial id)"
   echo
   echo "  Display Isabelle version information."
   echo
   exit 1
 }
 
 function fail()
 {
   echo "$1" >&2
   exit 2
 }
 
 
 ## process command line
 
 # options
 
 SHORT_ID=""
 TAGS=""
 
 while getopts "it" OPT
 do
   case "$OPT" in
     i)
       SHORT_ID=true
       ;;
     t)
       TAGS=true
       ;;
     \?)
       usage
       ;;
   esac
 done
 
 shift $(($OPTIND - 1))
 
 
 # args
 
 [ "$#" -ne 0 ] && usage
 
 
 ## main
 
 if [ -z "$SHORT_ID" -a -z "$TAGS" ]; then
   echo 'repository version'    # filled in automatically!
 fi
 
+HG_ARCHIVAL="$ISABELLE_HOME/.hg_archival.txt"
+
 if [ -n "$SHORT_ID" ]; then
   if [ -d "$ISABELLE_HOME/.hg" ]; then
     "${HG:-hg}" -R "$ISABELLE_HOME" log -r "p1()" --template="{node|short}\n" 2>/dev/null || exit "$?"
-  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
-    RESULT="$(fgrep node: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2 | head -c12)"
+  elif [ -f "$HG_ARCHIVAL" ]; then
+    RESULT="$(fgrep node: < "$HG_ARCHIVAL" | cut -d " " -f2 | head -c12)"
     [ -n "$RESULT" ] && echo "$RESULT"
   elif [ -n "$ISABELLE_ID" ]; then
     echo "$ISABELLE_ID"
   fi
 fi
 
 if [ -n "$TAGS" ]; then
   RESULT=""
   if [ -d "$ISABELLE_HOME/.hg" ]; then
     RESULT=$("${HG:-hg}" -R "$ISABELLE_HOME" id -t 2>/dev/null)
     RC="$?"
-  elif [ -f "$ISABELLE_HOME/.hg_archival.txt" ]; then
-    RESULT="$(fgrep tag: < "$ISABELLE_HOME/.hg_archival.txt" | cut -d " " -f2)"
+  elif [ -f "$HG_ARCHIVAL" ]; then
+    RESULT="$(fgrep tag: < "$HG_ARCHIVAL" | cut -d " " -f2)"
     RC="$?"
   fi
   if [ "$RC" -ne 0 ]; then
     exit "$RC"
   elif [ -n "$RESULT" -a "$RESULT" != "tip" ]; then
     echo "$RESULT"
   fi
 fi