# HG changeset patch
# User wenzelm
# Date 1223129109 -7200
# Node ID 4b79e5d3d0aa4b919153cc04a48ba9864c28baba
# Parent  eff93bc3c14fa50c928888dce693b24b0a5e0fda
replaced ISATOOL by ISABELLE_TOOL;

diff -r eff93bc3c14f -r 4b79e5d3d0aa Admin/Benchmarks/IsaMakefile
--- a/Admin/Benchmarks/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/Benchmarks/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -20,14 +20,14 @@
 ## HOL-datatype
 
 HOL:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
 
 HOL-datatype: HOL $(LOG)/HOL-datatype.gz
 
 $(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/Brackin.thy \
   HOL-datatype/Instructions.thy HOL-datatype/SML.thy \
   HOL-datatype/Verilog.thy
-	@$(ISATOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
+	@$(ISABELLE_TOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa Admin/build
--- a/Admin/build	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/build	Sat Oct 04 16:05:09 2008 +0200
@@ -17,12 +17,12 @@
 ISABELLE_DIR="$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd ..; pwd)"
 
 if [ -d "$ISABELLE_DIR/Distribution" ]; then
-  ISATOOL="$ISABELLE_DIR/Distribution/bin/isatool"
+  ISABELLE_TOOL="$ISABELLE_DIR/Distribution/bin/isatool"
   ISABELLE_LIB="$ISABELLE_DIR/Distribution/lib"
   ISABELLE_SRC="$ISABELLE_DIR"
   ISABELLE_DOC_SRC="$ISABELLE_DIR/Doc"
 else
-  ISATOOL="$ISABELLE_DIR/bin/isatool"
+  ISABELLE_TOOL="$ISABELLE_DIR/bin/isatool"
   ISABELLE_LIB="$ISABELLE_DIR/lib"
   ISABELLE_SRC="$ISABELLE_DIR/src"
   ISABELLE_DOC_SRC="$ISABELLE_DIR/doc-src"
@@ -112,7 +112,7 @@
   type -p scalac >/dev/null || fail "Scala compiler unavailable"
 
   pushd "$ISABELLE_SRC/Pure" >/dev/null
-  "$ISATOOL" make jar || fail "Failed to build Pure.jar!"
+  "$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
   popd >/dev/null
 
   if [ -d "$HOME/lib/jedit/current" ]; then
diff -r eff93bc3c14f -r 4b79e5d3d0aa Admin/isatest/isatest-annomaly
--- a/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/isatest/isatest-annomaly	Sat Oct 04 16:05:09 2008 +0200
@@ -42,7 +42,7 @@
 ## main
 
 ISABELLE_HOME="$DISTPREFIX/Isabelle"
-ISATOOL="$ISABELLE_HOME/bin/isatool"
+ISABELLE_TOOL="$ISABELLE_HOME/bin/isatool"
 
 [ -d $ISABELLE_HOME ] || fail "$ISABELLE_HOME is not a directory."
 
@@ -73,7 +73,7 @@
 do
   ( cd "$ISABELLE_HOME/src/$L"; \
     cat ~/settings/annomaly >> $ISABELLE_HOME/etc/settings; \
-    "$ISATOOL" make || fail "isatool make for $L failed." )
+    "$ISABELLE_TOOL" make || fail "isabelle make for $L failed." )
 done
 
 
diff -r eff93bc3c14f -r 4b79e5d3d0aa Admin/isatest/isatest-doc
--- a/Admin/isatest/isatest-doc	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/isatest/isatest-doc	Sat Oct 04 16:05:09 2008 +0200
@@ -25,7 +25,7 @@
 SHORT=at-poly
 SETTINGS=~/settings/$SHORT
 
-ISATOOL=$ISABELLE_DEVEL/bin/isatool
+ISABELLE_TOOL=$ISABELLE_DEVEL/bin/isatool
     
 
 MAIL=$HOME/bin/pmail
@@ -80,7 +80,7 @@
     (
       cd $DIR
       ulimit -t $MAXTIME 
-      nice $ISATOOL make >> $LOG 2>&1
+      nice $ISABELLE_TOOL make >> $LOG 2>&1
     ) || FAIL="${FAIL}${DIR} "    
     echo "Finished [$DIR]" >> $LOG
     echo >> $LOG
diff -r eff93bc3c14f -r 4b79e5d3d0aa Admin/isatest/isatest-makeall
--- a/Admin/isatest/isatest-makeall	Sat Oct 04 16:05:08 2008 +0200
+++ b/Admin/isatest/isatest-makeall	Sat Oct 04 16:05:09 2008 +0200
@@ -88,9 +88,9 @@
         ;;
 esac
 
-ISATOOL="$DISTPREFIX/Isabelle/bin/isatool"
+ISABELLE_TOOL="$DISTPREFIX/Isabelle/bin/isatool"
 
-[ -x $ISATOOL ] || fail "Cannot run $ISATOOL"
+[ -x $ISABELLE_TOOL ] || fail "Cannot run $ISABELLE_TOOL"
 
 if [ "$1" = "-l" ]; then
   shift
@@ -98,12 +98,12 @@
   LOGIC="$1"
   TARGETS="$2"
   shift 2
-  ISABELLE_HOME="$($ISATOOL getenv -b ISABELLE_HOME)"
+  ISABELLE_HOME="$($ISABELLE_TOOL getenv -b ISABELLE_HOME)"
   DIR="$ISABELLE_HOME/src/$LOGIC"
-  TOOL="$ISATOOL make $MFLAGS $TARGETS"
+  TOOL="$ISABELLE_TOOL make $MFLAGS $TARGETS"
 else
   DIR="."
-  TOOL="$ISATOOL makeall $MFLAGS all"
+  TOOL="$ISABELLE_TOOL makeall $MFLAGS all"
 fi
 
 # main test loop
diff -r eff93bc3c14f -r 4b79e5d3d0aa build
--- a/build	Sat Oct 04 16:05:08 2008 +0200
+++ b/build	Sat Oct 04 16:05:09 2008 +0200
@@ -175,7 +175,7 @@
 
 for L in $MAKE_LOGICS
 do
-  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make $TARGETS )
+  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make $TARGETS )
 done
 
 echo -n "Finished at "; date
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/AxClass/IsaMakefile
--- a/doc-src/AxClass/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/AxClass/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -13,7 +13,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -d false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
 
 
 ## Group
@@ -21,7 +21,7 @@
 Group: HOL $(LOG)/HOL-Group.gz
 
 HOL:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
 
 $(LOG)/HOL-Group.gz: $(OUT)/HOL Group/ROOT.ML Group/Group.thy \
   Group/Product.thy Group/Semigroups.thy
@@ -34,7 +34,7 @@
 Nat: FOL $(LOG)/FOL-Nat.gz
 
 FOL:
-	@cd $(SRC)/FOL; $(ISATOOL) make FOL
+	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
 
 $(LOG)/FOL-Nat.gz: $(OUT)/FOL Nat/ROOT.ML Nat/NatClass.thy
 	@$(USEDIR) $(OUT)/FOL Nat
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarAdvanced/Classes/IsaMakefile
--- a/doc-src/IsarAdvanced/Classes/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## Thy
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarAdvanced/Codegen/IsaMakefile
--- a/doc-src/IsarAdvanced/Codegen/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## Thy
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarAdvanced/Functions/IsaMakefile
--- a/doc-src/IsarAdvanced/Functions/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarAdvanced/Functions/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## Thy
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarImplementation/IsaMakefile
--- a/doc-src/IsarImplementation/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarImplementation/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## Thy
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarOverview/IsaMakefile
--- a/doc-src/IsarOverview/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarOverview/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -7,7 +7,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i false -g false -d false -D document -v true
+USEDIR = $(ISABELLE_TOOL) usedir -i false -g false -d false -D document -v true
 
 
 ## Isar
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/IsarRef/IsaMakefile
--- a/doc-src/IsarRef/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/IsarRef/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## IsarRef sessions
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/LaTeXsugar/IsaMakefile
--- a/doc-src/LaTeXsugar/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/LaTeXsugar/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -g false -d false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -g false -d false -D document
 
 
 ## Sugar
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/Locales/IsaMakefile
--- a/doc-src/Locales/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/Locales/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -13,7 +13,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -d false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -d false -D document
 
 
 ## Locales
@@ -21,7 +21,7 @@
 Locales: $(LOG)/HOL-Locales.gz
 
 HOL:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
 
 $(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Examples.thy \
   Locales/Examples1.thy Locales/Examples2.thy Locales/Examples3.thy \
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/System/IsaMakefile
--- a/doc-src/System/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/System/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -14,7 +14,7 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 
-USEDIR = $(ISATOOL) usedir -v true -i false -d false -C false -D document
+USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
 
 
 ## IsarRef sessions
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/System/Thy/Basics.thy
--- a/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/System/Thy/Basics.thy	Sat Oct 04 16:05:09 2008 +0200
@@ -126,7 +126,7 @@
 
   \begin{itemize}
 
-  \item @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
+  \item @{setting_def ISABELLE} and @{setting_def ISABELLE_TOOL} are set
   automatically to the absolute path names of the @{executable
   "isabelle-process"} and @{executable isatool} executables,
   respectively.
@@ -169,7 +169,7 @@
   a private @{verbatim "$ISABELLE_HOME_USER/etc/settings"}.
   
   \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
-  ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
+  ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   names of the @{executable "isabelle-process"} and @{executable
   isatool} executables, respectively.  Thus other tools and scripts
   need not assume that the @{"file" "$ISABELLE_HOME/bin"} directory is
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -18,19 +18,19 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 OPTIONS = -m brackets -i true -d "" -D document
-USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/HOL
+USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/HOL
 
 
 ## HOL
 
 HOL:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
 
 styles:
 	@rm -f isabelle.sty
 	@rm -f isabellesym.sty
 	@rm -f pdfsetup.sty
-	@$(ISATOOL) latex -o sty >/dev/null
+	@$(ISABELLE_TOOL) latex -o sty >/dev/null
 	@rm -f pdfsetup.sty
 	@rm -f */document/isabelle.sty
 	@rm -f */document/isabellesym.sty
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/TutorialI/Overview/IsaMakefile
--- a/doc-src/TutorialI/Overview/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/TutorialI/Overview/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -7,7 +7,7 @@
 SRC = $(ISABELLE_HOME)/src
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
-USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
+USEDIR = $(ISABELLE_TOOL) usedir -i true -d ps -D document -v true
 
 
 ## LNCS
diff -r eff93bc3c14f -r 4b79e5d3d0aa doc-src/ZF/IsaMakefile
--- a/doc-src/ZF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/doc-src/ZF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -16,19 +16,19 @@
 OUT = $(ISABELLE_OUTPUT)
 LOG = $(OUT)/log
 OPTIONS = -m brackets -i true -d "" -D document
-USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/ZF
+USEDIR = @$(ISABELLE_TOOL) usedir $(OPTIONS) $(OUT)/ZF
 
 
 ## ZF
 
 ZF:
-	@cd $(SRC)/ZF; $(ISATOOL) make ZF
+	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
 
 styles:
 	@rm -f isabelle.sty
 	@rm -f isabellesym.sty
 	@rm -f pdfsetup.sty
-	@$(ISATOOL) latex -o sty >/dev/null
+	@$(ISABELLE_TOOL) latex -o sty >/dev/null
 	@rm -f pdfsetup.sty
 	@rm -f document/isabelle.sty
 	@rm -f document/isabellesym.sty
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/browser
--- a/lib/Tools/browser	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/browser	Sat Oct 04 16:05:09 2008 +0200
@@ -65,7 +65,7 @@
 
 if [ -z "$GRAPHFILE" ]; then
   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
-  exec "$ISATOOL" java GraphBrowser.GraphBrowser
+  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
 else
   PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
   if [ -n "$CLEAN" ]; then
@@ -83,9 +83,9 @@
   esac
 
   if [ -z "$OUTFILE" ]; then
-    "$ISATOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
+    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(jvmpath "$PRIVATE_FILE")"
   else
-    "$ISATOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
+    "$ISABELLE_TOOL" java GraphBrowser.Console "$(jvmpath "$PRIVATE_FILE")" "$(jvmpath "$OUTFILE")"
   fi
   RC="$?"
 
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/doc
--- a/lib/Tools/doc	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/doc	Sat Oct 04 16:05:09 2008 +0200
@@ -53,7 +53,7 @@
     [ -d "$DIR" ] || fail "Bad document directory: $DIR"
     for FMT in "$ISABELLE_DOC_FORMAT" dvi
     do
-      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISATOOL" display "$DOC.$FMT"; }
+      [ -f "$DIR/$DOC.$FMT" ] && { cd "$DIR"; exec "$ISABELLE_TOOL" display "$DOC.$FMT"; }
     done
   done
   IFS="$ORIG_IFS"
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/document
--- a/lib/Tools/document	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/document	Sat Oct 04 16:05:09 2008 +0200
@@ -119,11 +119,11 @@
 {
   local FMT="$1"
   [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
-  "$ISATOOL" latex -o sty && \
-  "$ISATOOL" latex -o "$FMT" && \
-  { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
-  { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \
-  "$ISATOOL" latex -o "$FMT"
+  "$ISABELLE_TOOL" latex -o sty && \
+  "$ISABELLE_TOOL" latex -o "$FMT" && \
+  { [ ! -f root.bib ] || "$ISABELLE_TOOL" latex -o bbl; } && \
+  { [ ! -f root.idx ] || "$ISABELLE_TOOL" latex -o idx; } && \
+  "$ISABELLE_TOOL" latex -o "$FMT"
 }
 
 (
@@ -134,15 +134,15 @@
   prep_tags
 
   if [ -f IsaMakefile ]; then
-    "$ISATOOL" make "$OUTFORMAT"
+    "$ISABELLE_TOOL" make "$OUTFORMAT"
     RC="$?"
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \
-    "$ISATOOL" latex -o pdf
+    "$ISABELLE_TOOL" latex -o pdf
     RC="$?"
   else
     pre_latex dvi && \
-    "$ISATOOL" latex -o "$OUTFORMAT"
+    "$ISABELLE_TOOL" latex -o "$OUTFORMAT"
     RC="$?"
   fi
 
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/makeall
--- a/lib/Tools/makeall	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/makeall	Sat Oct 04 16:05:09 2008 +0200
@@ -41,7 +41,7 @@
 
 for L in $ALL_LOGICS
 do
-  ( cd "$ISABELLE_HOME/src/$L"; "$ISATOOL" make "$@" ) || FAIL="$FAIL$L "
+  ( cd "$ISABELLE_HOME/src/$L"; "$ISABELLE_TOOL" make "$@" ) || FAIL="$FAIL$L "
 done
 
 echo -n "Finished at "; date
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/mkdir
--- a/lib/Tools/mkdir	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/mkdir	Sat Oct 04 16:05:09 2008 +0200
@@ -137,7 +137,7 @@
     echo "OUT = \$(ISABELLE_OUTPUT)"
     echo "LOG = \$(OUT)/log"
     echo
-    echo "USEDIR = \$(ISATOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
+    echo "USEDIR = \$(ISABELLE_TOOL) usedir ${VERBOSE}-i true -d $ISABELLE_DOC_FORMAT  ## -D generated"
     echo
     echo
     echo "## $NAME"
@@ -146,7 +146,7 @@
       echo "$NAME: $LOGIC $TARGET"
       echo
       echo "$LOGIC:"
-      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISATOOL) make $LOGIC"
+      echo -e "\t@cd \$(SRC)/$LOGIC; \$(ISABELLE_TOOL) make $LOGIC"
       echo
       echo "$TARGET: \$(OUT)/$LOGIC $ROOT_ML $DOCUMENT_ROOT ## $SOURCES"
       echo -e "\t@$USEDIR \$(OUT)/$LOGIC $NAME"
diff -r eff93bc3c14f -r 4b79e5d3d0aa lib/Tools/mkproject
--- a/lib/Tools/mkproject	Sat Oct 04 16:05:08 2008 +0200
+++ b/lib/Tools/mkproject	Sat Oct 04 16:05:09 2008 +0200
@@ -22,6 +22,5 @@
   usage
 fi
 
-"$ISATOOL" mkdir -b -q "$NAME"
-(cd document; "$ISATOOL" latex -o sty)
-
+"$ISABELLE_TOOL" mkdir -b -q "$NAME"
+( cd document; "$ISABELLE_TOOL" latex -o sty; )
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/CCL/IsaMakefile
--- a/src/CCL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/CCL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,13 +24,13 @@
 CCL: FOL $(OUT)/CCL
 
 FOL:
-	@cd $(SRC)/FOL; $(ISATOOL) make FOL
+	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
 
 $(OUT)/FOL: FOL
 
 $(OUT)/CCL: $(OUT)/FOL CCL.thy Fix.thy Gfp.thy Hered.thy Lfp.thy ROOT.ML \
   Set.thy Term.thy Trancl.thy Type.thy Wfd.thy
-	@$(ISATOOL) usedir -b -r $(OUT)/FOL CCL
+	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL CCL
 
 
 ## CCL-ex
@@ -39,7 +39,7 @@
 
 $(LOG)/CCL-ex.gz: $(OUT)/CCL ex/Flag.thy ex/List.thy ex/Nat.thy ex/ROOT.ML \
   ex/Stream.thy
-	@$(ISATOOL) usedir $(OUT)/CCL ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/CCL ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/CTT/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,11 +24,11 @@
 CTT: Pure $(OUT)/CTT
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/CTT: $(OUT)/Pure $(SRC)/Provers/typedsimp.ML Arith.thy \
   Bool.thy CTT.thy Main.thy ROOT.ML rew.ML
-	@$(ISATOOL) usedir -b $(OUT)/Pure CTT
+	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure CTT
 
 
 ## CTT-ex
@@ -37,7 +37,7 @@
 
 $(LOG)/CTT-ex.gz: $(OUT)/CTT ex/ROOT.ML ex/Elimination.thy \
   ex/Equality.thy ex/Synthesis.thy ex/Typechecking.thy
-	@$(ISATOOL) usedir $(OUT)/CTT ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/CTT ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Cube/IsaMakefile
--- a/src/Cube/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Cube/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,10 +24,10 @@
 Pure-Cube: Pure $(LOG)/Pure-Cube.gz
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(LOG)/Pure-Cube.gz: $(OUT)/Pure Cube.thy Example.thy ROOT.ML
-	@cd ..; $(ISATOOL) usedir $(OUT)/Pure Cube
+	@cd ..; $(ISABELLE_TOOL) usedir $(OUT)/Pure Cube
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/FOL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,7 +24,7 @@
 FOL: Pure $(OUT)/FOL
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/Pure: Pure
 
@@ -38,7 +38,7 @@
   $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy	\
   IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex		\
   fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
-	@$(ISATOOL) usedir -p 2 -b $(OUT)/Pure FOL
+	@$(ISABELLE_TOOL) usedir -p 2 -b $(OUT)/Pure FOL
 
 
 ## FOL-ex
@@ -51,7 +51,7 @@
   ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
   ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
   ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
-	@$(ISATOOL) usedir $(OUT)/FOL ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/FOLP/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,11 +24,11 @@
 FOLP: Pure $(OUT)/FOLP
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/FOLP: $(OUT)/Pure FOLP.thy IFOLP.thy ROOT.ML classical.ML	\
   hypsubst.ML intprover.ML simp.ML simpdata.ML
-	@$(ISATOOL) usedir -b $(OUT)/Pure FOLP
+	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure FOLP
 
 
 ## FOLP-ex
@@ -40,7 +40,7 @@
   ex/Prolog.ML ex/Prolog.thy ex/Propositional_Int.thy			\
   ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
   ex/Quantifiers_Cla.thy
-	@$(ISATOOL) usedir $(OUT)/FOLP ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/FOLP ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/HOL/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -69,7 +69,7 @@
 HOL-Main: Pure $(OUT)/HOL-Main
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/Pure: Pure
 
@@ -182,7 +182,7 @@
   $(SRC)/Tools/rat.ML
 
 $(OUT)/HOL-Plain: plain.ML $(PLAIN_DEPENDENCIES)
-	@$(ISATOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
+	@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
 
 MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
   Arith_Tools.thy \
@@ -247,7 +247,7 @@
   Tools/TFL/utils.ML
 
 $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
-	@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
+	@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
 
 $(OUT)/HOL: ROOT.ML $(MAIN_DEPENDENCIES) \
   Complex/Complex_Main.thy \
@@ -285,7 +285,7 @@
   Tools/Qelim/ferrante_rackoff.ML \
   Tools/Qelim/langford_data.ML \
   Tools/Qelim/langford.ML
-	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
+	@$(ISABELLE_TOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
 
 
 ## HOL-Library
@@ -320,7 +320,7 @@
   Library/Assert.thy Library/Relational.thy Library/Sublist.thy Library/Subarray.thy	\
   Library/Ref.thy Library/Imperative_HOL.thy Library/RBT.thy		\
   Library/Enum.thy Real/Float.thy $(SRC)/Tools/float.ML
-	@cd Library; $(ISATOOL) usedir $(OUT)/HOL Library
+	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
 
 ## HOL-HahnBanach
@@ -337,7 +337,7 @@
   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy		\
   Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib	\
   Real/HahnBanach/document/root.tex
-	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL HahnBanach
+	@cd Real; $(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HahnBanach
 
 
 ## HOL-Subst
@@ -346,7 +346,7 @@
 
 $(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML		\
   Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
-	@$(ISATOOL) usedir $(OUT)/HOL Subst
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
 
 
 ## HOL-Induct
@@ -359,7 +359,7 @@
   Induct/QuoDataType.thy Induct/ROOT.ML Induct/Sexp.thy			\
   Induct/Sigma_Algebra.thy Induct/SList.thy Induct/ABexp.thy		\
   Induct/Term.thy Induct/Tree.thy Induct/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOL Induct
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Induct
 
 
 ## HOL-IMP
@@ -370,7 +370,7 @@
   IMP/Compiler.thy IMP/Denotation.thy IMP/Expr.thy IMP/Hoare.thy	\
   IMP/Natural.thy IMP/Examples.thy IMP/Transition.thy IMP/VC.thy	\
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
-	@$(ISATOOL) usedir -g true $(OUT)/HOL IMP
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL IMP
 
 
 ## HOL-IMPP
@@ -379,7 +379,7 @@
 
 $(LOG)/HOL-IMPP.gz: $(OUT)/HOL IMPP/ROOT.ML IMPP/Com.thy		\
   IMPP/Natural.thy IMPP/Hoare.thy IMPP/Misc.thy IMPP/EvenOdd.thy
-	@$(ISATOOL) usedir $(OUT)/HOL IMPP
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IMPP
 
 
 ## HOL-Import
@@ -397,7 +397,7 @@
 HOL-Import: HOL $(LOG)/HOL-Import.gz
 
 $(LOG)/HOL-Import.gz: $(OUT)/HOL $(IMPORTER_FILES)
-	@$(ISATOOL) usedir $(OUT)/HOL Import
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import
 
 
 ## HOL-Generate-HOL
@@ -410,7 +410,7 @@
   Import/Generate-HOL/GenHOL4Real.thy					\
   Import/Generate-HOL/GenHOL4Vec.thy					\
   Import/Generate-HOL/GenHOL4Word32.thy Import/Generate-HOL/ROOT.ML
-	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOL
+	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOL
 
 
 ## HOL-Generate-HOLLight
@@ -420,7 +420,7 @@
 $(LOG)/HOL-Generate-HOLLight.gz: $(OUT)/HOL		\
   $(IMPORTER_HOLLIGHT_FILES) Import/Generate-HOLLight/GenHOLLight.thy	\
   Import/Generate-HOLLight/ROOT.ML
-	@cd Import; $(ISATOOL) usedir $(OUT)/HOL Generate-HOLLight
+	@cd Import; $(ISABELLE_TOOL) usedir $(OUT)/HOL Generate-HOLLight
 
 
 ## HOL-Import-HOL
@@ -443,14 +443,14 @@
   Import/HOL/HOL4Prob.thy Import/HOL/HOL4Real.thy			\
   Import/HOL/HOL4Vec.thy Import/HOL/HOL4Word32.thy Import/HOL/HOL4.thy	\
   Import/HOL/ROOT.ML
-	@cd Import/HOL; $(ISATOOL) usedir -b $(OUT)/HOL HOL4
+	@cd Import/HOL; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOL4
 
 HOLLight: HOL $(LOG)/HOLLight.gz
 
 $(LOG)/HOLLight.gz: $(OUT)/HOL $(IMPORTER_HOLLIGHT_FILES)	\
   Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
   Import/HOLLight/ROOT.ML
-	@cd Import/HOLLight; $(ISATOOL) usedir -b $(OUT)/HOL HOLLight
+	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
 
 
 ## HOL-NumberTheory
@@ -468,7 +468,7 @@
   NumberTheory/Euler.thy NumberTheory/Gauss.thy				\
   NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
   NumberTheory/ROOT.ML
-	@$(ISATOOL) usedir -g true $(OUT)/HOL NumberTheory
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
 
 
 ## HOL-Hoare
@@ -481,7 +481,7 @@
   Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy			\
   Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy	\
   Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
-	@$(ISATOOL) usedir $(OUT)/HOL Hoare
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
 
 
 ## HOL-HoareParallel
@@ -498,7 +498,7 @@
   HoareParallel/RG_Syntax.thy HoareParallel/RG_Tran.thy			\
   HoareParallel/ROOT.ML HoareParallel/document/root.tex			\
   HoareParallel/document/root.bib
-	@$(ISATOOL) usedir -g true $(OUT)/HOL HoareParallel
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL HoareParallel
 
 
 ## HOL-MetisExamples
@@ -510,7 +510,7 @@
   MetisExamples/BT.thy MetisExamples/Message.thy		\
   MetisExamples/Tarski.thy MetisExamples/TransClosure.thy	\
   MetisExamples/set.thy
-	@$(ISATOOL) usedir $(OUT)/HOL MetisExamples
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL MetisExamples
 
 
 ## HOL-Algebra
@@ -533,7 +533,7 @@
   Algebra/document/root.tex Algebra/poly/LongDiv.thy			\
   Algebra/poly/PolyHomo.thy Algebra/poly/Polynomial.thy			\
   Algebra/poly/UnivPoly2.thy Algebra/ringsimp.ML
-	@cd Algebra; $(ISATOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
+	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
 
 
 ## HOL-Auth
@@ -557,7 +557,7 @@
   Auth/Guard/Guard_Yahalom.thy Auth/Smartcard/EventSC.thy		\
   Auth/Smartcard/ShoupRubinBella.thy Auth/Smartcard/ShoupRubin.thy	\
   Auth/Smartcard/Smartcard.thy Auth/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL Auth
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Auth
 
 
 ## HOL-UNITY
@@ -582,7 +582,7 @@
   UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy			\
   UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy			\
   UNITY/Comp/TimerArray.thy UNITY/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL UNITY
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL UNITY
 
 
 ## HOL-Unix
@@ -592,7 +592,7 @@
 $(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy	\
   Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy		\
   Unix/document/root.bib Unix/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOL Unix
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Unix
 
 
 ## HOL-ZF
@@ -601,7 +601,7 @@
 
 $(LOG)/HOL-ZF.gz: $(OUT)/HOL ZF/ROOT.ML ZF/Helper.thy ZF/LProd.thy	\
   ZF/HOLZF.thy ZF/MainZF.thy ZF/Games.thy ZF/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOL ZF
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ZF
 
 
 ## HOL-Modelcheck
@@ -613,7 +613,7 @@
   Modelcheck/MuCalculus.thy Modelcheck/MuckeExample1.thy	\
   Modelcheck/MuckeExample2.thy Modelcheck/MuckeSyn.thy		\
   Modelcheck/ROOT.ML Modelcheck/mucke_oracle.ML
-	@$(ISATOOL) usedir $(OUT)/HOL Modelcheck
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Modelcheck
 
 
 ## HOL-SizeChange
@@ -626,7 +626,7 @@
   SizeChange/Interpretation.thy SizeChange/Implementation.thy		\
   SizeChange/Size_Change_Termination.thy SizeChange/Examples.thy	\
   SizeChange/sct.ML SizeChange/ROOT.ML
-	@$(ISATOOL) usedir $(OUT)/HOL SizeChange
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL SizeChange
 
 
 ## HOL-Lambda
@@ -639,7 +639,7 @@
   Lambda/ParRed.thy Lambda/Standardization.thy Lambda/StrongNorm.thy	\
   Lambda/Type.thy Lambda/WeakNorm.thy Lambda/ROOT.ML			\
   Lambda/document/root.bib Lambda/document/root.tex
-	@$(ISATOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
+	@$(ISABELLE_TOOL) usedir -g true -m no_brackets $(OUT)/HOL Lambda
 
 
 ## HOL-Prolog
@@ -648,7 +648,7 @@
 
 $(LOG)/HOL-Prolog.gz: $(OUT)/HOL Prolog/ROOT.ML Prolog/prolog.ML	\
   Prolog/HOHH.thy Prolog/Test.thy Prolog/Func.thy Prolog/Type.thy
-	@$(ISATOOL) usedir $(OUT)/HOL Prolog
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
 
 
 ## HOL-W0
@@ -656,7 +656,7 @@
 HOL-W0: HOL $(LOG)/HOL-W0.gz
 
 $(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOL W0
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL W0
 
 
 ## HOL-MicroJava
@@ -692,7 +692,7 @@
   MicroJava/BV/LBVComplete.thy MicroJava/BV/LBVJVM.thy			\
   MicroJava/document/root.bib MicroJava/document/root.tex		\
   MicroJava/document/introduction.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL MicroJava
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL MicroJava
 
 
 ## HOL-NanoJava
@@ -703,7 +703,7 @@
   NanoJava/Decl.thy NanoJava/TypeRel.thy NanoJava/State.thy		\
   NanoJava/OpSem.thy NanoJava/AxSem.thy NanoJava/AxSem.thy		\
   NanoJava/document/root.bib NanoJava/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL NanoJava
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NanoJava
 
 
 ## HOL-Bali
@@ -718,7 +718,7 @@
   Bali/TypeRel.thy Bali/TypeSafe.thy Bali/Value.thy Bali/WellForm.thy	\
   Bali/DefiniteAssignment.thy Bali/DefiniteAssignmentCorrect.thy	\
   Bali/WellType.thy Bali/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL Bali
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Bali
 
 
 ## HOL-Extraction
@@ -731,7 +731,7 @@
   Extraction/QuotRem.thy Extraction/ROOT.ML Extraction/Util.thy	\
   Extraction/Warshall.thy Extraction/document/root.tex		\
   Extraction/document/root.bib
-	@$(ISATOOL) usedir $(OUT)/HOL Extraction
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Extraction
 
 
 ## HOL-IOA
@@ -740,7 +740,7 @@
 
 $(LOG)/HOL-IOA.gz: $(OUT)/HOL IOA/Asig.thy IOA/IOA.thy IOA/ROOT.ML	\
   IOA/Solve.thy
-	@$(ISATOOL) usedir $(OUT)/HOL IOA
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL IOA
 
 
 ## HOL-AxClasses
@@ -749,7 +749,7 @@
 
 $(LOG)/HOL-AxClasses.gz: $(OUT)/HOL AxClasses/Group.thy			\
   AxClasses/Product.thy AxClasses/ROOT.ML AxClasses/Semigroups.thy
-	@$(ISATOOL) usedir $(OUT)/HOL AxClasses
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL AxClasses
 
 
 ## HOL-Lattice
@@ -759,7 +759,7 @@
 $(LOG)/HOL-Lattice.gz: $(OUT)/HOL Lattice/Bounds.thy			\
   Lattice/CompleteLattice.thy Lattice/Lattice.thy Lattice/Orders.thy	\
   Lattice/ROOT.ML Lattice/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOL Lattice
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Lattice
 
 
 ## HOL-ex
@@ -796,7 +796,7 @@
   Complex/ex/Sqrt_Script.thy Complex/ex/MIR.thy Complex/ex/mirtac.ML	\
   Complex/ex/ReflectedFerrack.thy					\
   Complex/ex/linrtac.ML
-	@$(ISATOOL) usedir $(OUT)/HOL ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
 
 
 ## HOL-Isar_examples
@@ -814,7 +814,7 @@
   Isar_examples/ROOT.ML Isar_examples/document/proof.sty		\
   Isar_examples/document/root.bib Isar_examples/document/root.tex	\
   Isar_examples/document/style.tex Hoare/hoare_tac.ML
-	@$(ISATOOL) usedir $(OUT)/HOL Isar_examples
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Isar_examples
 
 
 ## HOL-SET-Protocol
@@ -826,7 +826,7 @@
   SET-Protocol/PublicSET.thy SET-Protocol/Cardholder_Registration.thy	\
   SET-Protocol/Merchant_Registration.thy SET-Protocol/Purchase.thy	\
   SET-Protocol/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL SET-Protocol
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL SET-Protocol
 
 
 ## HOL-Matrix
@@ -847,7 +847,7 @@
   Matrix/cplex/CplexMatrixConverter.ML Matrix/cplex/Cplex_tools.ML	\
   Matrix/cplex/FloatSparseMatrixBuilder.ML Matrix/cplex/fspmlp.ML	\
   Matrix/cplex/matrixlp.ML
-	@$(ISATOOL) usedir -g true $(OUT)/HOL Matrix
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Matrix
 
 
 ## TLA
@@ -856,7 +856,7 @@
 
 $(OUT)/TLA: $(OUT)/HOL TLA/Action.thy TLA/Init.thy TLA/Intensional.thy	\
   TLA/ROOT.ML TLA/Stfun.thy TLA/TLA.thy
-	@cd TLA; $(ISATOOL) usedir -b $(OUT)/HOL TLA
+	@cd TLA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL TLA
 
 
 ## TLA-Inc
@@ -864,7 +864,7 @@
 TLA-Inc: TLA $(LOG)/TLA-Inc.gz
 
 $(LOG)/TLA-Inc.gz: $(OUT)/TLA TLA/Inc/Inc.thy
-	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Inc
+	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Inc
 
 
 ## TLA-Buffer
@@ -872,7 +872,7 @@
 TLA-Buffer: TLA $(LOG)/TLA-Buffer.gz
 
 $(LOG)/TLA-Buffer.gz: $(OUT)/TLA TLA/Buffer/Buffer.thy TLA/Buffer/DBuffer.thy
-	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Buffer
+	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Buffer
 
 
 ## TLA-Memory
@@ -884,7 +884,7 @@
   TLA/Memory/MemoryImplementation.thy TLA/Memory/MemoryParameters.thy	\
   TLA/Memory/ProcedureInterface.thy TLA/Memory/RPC.thy			\
   TLA/Memory/RPCMemoryParams.thy TLA/Memory/RPCParameters.thy
-	@cd TLA; $(ISATOOL) usedir $(OUT)/TLA Memory
+	@cd TLA; $(ISABELLE_TOOL) usedir $(OUT)/TLA Memory
 
 
 ## HOL-Nominal
@@ -902,7 +902,7 @@
   Nominal/nominal_primrec.ML \
   Nominal/nominal_thmdecls.ML \
   Library/Infinite_Set.thy
-	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
+	@cd Nominal; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal
 
 
 ## HOL-Nominal-Examples
@@ -931,7 +931,7 @@
   Nominal/Examples/VC_Condition.thy \
   Nominal/Examples/W.thy \
   Nominal/Examples/Weakening.thy
-	@cd Nominal; $(ISATOOL) usedir $(OUT)/HOL-Nominal Examples
+	@cd Nominal; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Nominal Examples
 
 
 ## HOL-Word
@@ -946,7 +946,7 @@
   Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
   Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
   Word/document/root.bib
-	@cd Word; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Word
+	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 
 
 ## HOL-Word-Examples
@@ -955,7 +955,7 @@
 
 $(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word Word/Examples/ROOT.ML	\
   Word/Examples/WordExamples.thy
-	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
+	@cd Word; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Word Examples
 
 
 ## HOL-Statespace
@@ -967,7 +967,7 @@
   Statespace/StateSpaceSyntax.thy Statespace/StateSpaceEx.thy		\
   Statespace/distinct_tree_prover.ML Statespace/state_space.ML		\
   Statespace/state_fun.ML Statespace/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Statespace
 
 
 ## HOL-NSA
@@ -999,7 +999,7 @@
   Library/Infinite_Set.thy \
   Library/Zorn.thy \
   NSA/ROOT.ML
-	@cd NSA; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
+	@cd NSA; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-NSA
 
 
 ## HOL-NSA-Examples
@@ -1008,7 +1008,7 @@
 
 $(LOG)/HOL-NSA-Examples.gz: $(OUT)/HOL-NSA NSA/Examples/ROOT.ML	\
   NSA/Examples/NSPrimes.thy
-	@cd NSA; $(ISATOOL) usedir $(OUT)/HOL-NSA Examples
+	@cd NSA; $(ISABELLE_TOOL) usedir $(OUT)/HOL-NSA Examples
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/HOLCF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -25,7 +25,7 @@
 HOLCF: HOL $(OUT)/HOLCF
 
 HOL:
-	@cd $(SRC)/HOL; $(ISATOOL) make HOL
+	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
 
 $(OUT)/HOLCF: $(OUT)/HOL \
   ROOT.ML \
@@ -71,7 +71,7 @@
   Tools/pcpodef_package.ML \
   holcf_logic.ML \
   document/root.tex
-	@$(ISATOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
+	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/HOL HOLCF
 
 
 ## HOLCF-IMP
@@ -80,7 +80,7 @@
 
 $(LOG)/HOLCF-IMP.gz: $(OUT)/HOLCF IMP/HoareEx.thy \
   IMP/Denotational.thy IMP/ROOT.ML IMP/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/HOLCF IMP
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF IMP
 
 
 ## HOLCF-ex
@@ -90,7 +90,7 @@
 $(LOG)/HOLCF-ex.gz: $(OUT)/HOLCF ex/Stream.thy ex/Dagstuhl.thy \
   ex/Dnat.thy ex/Fix2.thy ex/Focus_ex.thy ex/Hoare.thy ex/Loop.thy \
   ex/ROOT.ML ex/Fixrec_ex.thy ../HOL/Library/Nat_Infinity.thy
-	@$(ISATOOL) usedir $(OUT)/HOLCF ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF ex
 
 
 ## HOLCF-FOCUS
@@ -101,7 +101,7 @@
   FOCUS/Fstream.thy FOCUS/FOCUS.thy \
   FOCUS/Stream_adm.thy ../HOL/Library/Continuity.thy \
   FOCUS/Buffer.thy FOCUS/Buffer_adm.thy
-	@$(ISATOOL) usedir $(OUT)/HOLCF FOCUS
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOLCF FOCUS
 
 ## IOA
 
@@ -118,7 +118,7 @@
   IOA/meta_theory/LiveIOA.thy IOA/meta_theory/Pred.thy		       \
   IOA/meta_theory/Abstraction.thy IOA/meta_theory/Simulations.thy      \
   IOA/meta_theory/SimCorrectness.thy IOA/meta_theory/ioa_package.ML
-	@cd IOA; $(ISATOOL) usedir -b $(OUT)/HOLCF IOA
+	@cd IOA; $(ISABELLE_TOOL) usedir -b $(OUT)/HOLCF IOA
 
 
 ## IOA-ABP
@@ -132,7 +132,7 @@
   IOA/ABP/Lemmas.thy IOA/ABP/Packet.thy \
   IOA/ABP/ROOT.ML IOA/ABP/Receiver.thy IOA/ABP/Sender.thy \
   IOA/ABP/Spec.thy
-	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ABP
+	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ABP
 
 ## IOA-NTP
 
@@ -143,7 +143,7 @@
   IOA/NTP/Impl.thy IOA/NTP/Lemmas.thy IOA/NTP/Multiset.thy \
   IOA/NTP/Packet.thy IOA/NTP/ROOT.ML IOA/NTP/Receiver.thy IOA/NTP/Sender.thy \
   IOA/NTP/Spec.thy
-	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA NTP
+	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA NTP
 
 
 ## IOA-Modelcheck
@@ -153,7 +153,7 @@
 $(LOG)/IOA-Modelcheck.gz: $(OUT)/IOA IOA/Modelcheck/ROOT.ML \
   IOA/Modelcheck/Cockpit.thy IOA/Modelcheck/MuIOA.thy \
   IOA/Modelcheck/MuIOAOracle.thy IOA/Modelcheck/Ring3.thy
-	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Modelcheck
+	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Modelcheck
 
 
 ## IOA-Storage
@@ -163,7 +163,7 @@
 $(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
   IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
   IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
-	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage
+	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA Storage
 
 
 ## IOA-ex
@@ -171,7 +171,7 @@
 IOA-ex: IOA $(LOG)/IOA-ex.gz
 
 $(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
-	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex
+	@cd IOA; $(ISABELLE_TOOL) usedir $(OUT)/IOA ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/LCF/IsaMakefile
--- a/src/LCF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/LCF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,10 +24,10 @@
 LCF: FOL $(OUT)/LCF
 
 FOL:
-	@cd $(SRC)/FOL; $(ISATOOL) make FOL
+	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
 
 $(OUT)/LCF: $(OUT)/FOL LCF.thy ROOT.ML
-	@$(ISATOOL) usedir -b -r $(OUT)/FOL LCF
+	@$(ISABELLE_TOOL) usedir -b -r $(OUT)/FOL LCF
 
 
 ## LCF-ex
@@ -35,7 +35,7 @@
 LCF-ex: LCF $(LOG)/LCF-ex.gz
 
 $(LOG)/LCF-ex.gz: $(OUT)/LCF ex/Ex1.thy ex/Ex2.thy ex/Ex3.thy ex/Ex4.thy ex/ROOT.ML
-	@$(ISATOOL) usedir $(OUT)/LCF ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/LCF ex
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Pure/General/file.ML	Sat Oct 04 16:05:09 2008 +0200
@@ -66,7 +66,7 @@
 
 (* system commands *)
 
-fun isabelle_tool cmd = system ("\"$ISATOOL\" " ^ cmd);
+fun isabelle_tool cmd = system ("\"$ISABELLE_TOOL\" " ^ cmd);
 
 fun system_command cmd =
   if system cmd <> 0 then error ("System command failed: " ^ cmd)
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Pure/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -92,7 +92,7 @@
 Pure-ProofGeneral: Pure $(LOG)/Pure-ProofGeneral.gz
 
 $(LOG)/Pure-ProofGeneral.gz: $(OUT)/Pure ProofGeneral/proof_general_keywords.ML
-	@$(ISATOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
+	@$(ISABELLE_TOOL) usedir -f proof_general_keywords.ML $(OUT)/Pure ProofGeneral
 
 
 RAW: $(OUT)/RAW
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Pure/Thy/present.ML	Sat Oct 04 16:05:09 2008 +0200
@@ -325,7 +325,7 @@
 
 fun isabelle_document verbose format name tags path result_path =
   let
-    val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
+    val s = "\"$ISABELLE_TOOL\" document -c -o '" ^ format ^ "' \
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
       " 2>&1" ^ (if verbose then "" else " >/dev/null");
     val doc_path = Path.append result_path (Path.ext format (Path.basic name));
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Pure/Tools/isabelle_system.scala
--- a/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 16:05:09 2008 +0200
@@ -93,7 +93,7 @@
 
   def isabelle_tool(args: String*) = {
     val proc =
-      try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) }
+      try { exec2((List(getenv_strict("ISABELLE_TOOL")) ++ args): _*) }
       catch { case e: IOException => error(e.getMessage) }
     proc.getOutputStream.close
     val output = Source.fromInputStream(proc.getInputStream, charset).mkString("")
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/Sequents/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -24,12 +24,12 @@
 Sequents: Pure $(OUT)/Sequents
 
 Pure:
-	@cd $(SRC)/Pure; $(ISATOOL) make Pure
+	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(OUT)/Sequents: $(OUT)/Pure ILL.thy LK0.thy LK.thy \
   modal.ML ROOT.ML simpdata.ML S4.thy S43.thy Sequents.thy T.thy prover.ML \
   ILL_predlog.thy Washing.thy
-	@$(ISATOOL) usedir -b $(OUT)/Pure Sequents
+	@$(ISABELLE_TOOL) usedir -b $(OUT)/Pure Sequents
 
 
 ## Sequents-LK
@@ -38,7 +38,7 @@
 
 $(LOG)/Sequents-LK.gz: $(OUT)/Sequents LK/ROOT.ML LK/Hard_Quantifiers.thy \
   LK/Propositional.thy LK/Quantifiers.thy LK/Nat.thy
-	@$(ISATOOL) usedir $(OUT)/Sequents LK
+	@$(ISABELLE_TOOL) usedir $(OUT)/Sequents LK
 
 
 ## clean
diff -r eff93bc3c14f -r 4b79e5d3d0aa src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Sat Oct 04 16:05:08 2008 +0200
+++ b/src/ZF/IsaMakefile	Sat Oct 04 16:05:09 2008 +0200
@@ -26,7 +26,7 @@
 ZF: FOL $(OUT)/ZF
 
 FOL:
-	@cd $(SRC)/FOL; $(ISATOOL) make FOL
+	@cd $(SRC)/FOL; $(ISABELLE_TOOL) make FOL
 
 $(OUT)/ZF: $(OUT)/FOL AC.thy Arith.thy ArithSimp.thy Bin.thy Bool.thy	\
   Cardinal.thy CardinalArith.thy Cardinal_AC.thy Datatype_ZF.thy	\
@@ -40,7 +40,7 @@
   Tools/primrec_package.ML Tools/typechk.ML Trancl.thy Univ.thy WF.thy	\
   ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy ind_syntax.ML	\
   int_arith.ML pair.thy simpdata.ML upair.thy
-	@$(ISATOOL) usedir -b -g true -r $(OUT)/FOL ZF
+	@$(ISABELLE_TOOL) usedir -b -g true -r $(OUT)/FOL ZF
 
 
 ## ZF-AC
@@ -52,7 +52,7 @@
   AC/AC_Equiv.thy AC/Cardinal_aux.thy AC/DC.thy AC/HH.thy		\
   AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy AC/WO2_AC16.thy		\
   AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/ZF AC
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF AC
 
 
 ## ZF-Coind
@@ -62,7 +62,7 @@
 $(LOG)/ZF-Coind.gz: $(OUT)/ZF Coind/Dynamic.thy Coind/ECR.thy		\
   Coind/Language.thy Coind/Map.thy Coind/ROOT.ML Coind/Static.thy	\
   Coind/Types.thy Coind/Values.thy
-	@$(ISATOOL) usedir $(OUT)/ZF Coind
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Coind
 
 
 ## ZF-Constructible
@@ -80,7 +80,7 @@
   Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy	\
   Constructible/Reflection.thy Constructible/WFrec.thy			\
   Constructible/document/root.bib Constructible/document/root.tex
-	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/ZF Constructible
 
 
 ## ZF-IMP
@@ -90,7 +90,7 @@
 $(LOG)/ZF-IMP.gz: $(OUT)/ZF IMP/Com.thy IMP/Denotation.thy	\
   IMP/Equiv.thy IMP/ROOT.ML IMP/document/root.bib		\
   IMP/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/ZF IMP
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF IMP
 
 
 ## ZF-Resid
@@ -100,7 +100,7 @@
 $(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy	\
   Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy		\
   Resid/Substitution.thy
-	@$(ISATOOL) usedir $(OUT)/ZF Resid
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Resid
 
 
 ## ZF-UNITY
@@ -114,7 +114,7 @@
   UNITY/ClientImpl.thy UNITY/Distributor.thy UNITY/Follows.thy		\
   UNITY/Increasing.thy UNITY/Merge.thy UNITY/Monotonicity.thy		\
   UNITY/MultisetSum.thy UNITY/WFair.thy
-	@$(ISATOOL) usedir $(OUT)/ZF UNITY
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF UNITY
 
 
 ## ZF-Induct
@@ -127,7 +127,7 @@
   Induct/Multiset.thy Induct/Mutil.thy Induct/Ntree.thy			\
   Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy			\
   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
-	@$(ISATOOL) usedir $(OUT)/ZF Induct
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF Induct
 
 
 ## ZF-ex
@@ -137,7 +137,7 @@
 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BinEx.thy ex/CoUnit.thy	\
   ex/Commutation.thy ex/Group.thy ex/Limit.thy ex/LList.thy		\
   ex/Primes.thy ex/NatSum.thy ex/Ramsey.thy ex/Ring.thy ex/misc.thy
-	@$(ISATOOL) usedir $(OUT)/ZF ex
+	@$(ISABELLE_TOOL) usedir $(OUT)/ZF ex
 
 
 ## clean