# HG changeset patch
# User wenzelm
# Date 1457627404 -3600
# Node ID b5783412bfed093ebea036da272c7c9370f325fb
# Parent  cd266473b81b55c46ab7177454828d144a2b4f8a
prefer plain "isabelle" from PATH within Isabelle settings environment;

diff -r cd266473b81b -r b5783412bfed Admin/lib/Tools/build_doc
--- a/Admin/lib/Tools/build_doc	Thu Mar 10 12:11:50 2016 +0100
+++ b/Admin/lib/Tools/build_doc	Thu Mar 10 17:30:04 2016 +0100
@@ -18,4 +18,4 @@
 
 declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_BUILD_JAVA_OPTIONS)"
 
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
+isabelle java "${JAVA_ARGS[@]}" isabelle.Build_Doc "$@"
diff -r cd266473b81b -r b5783412bfed Admin/lib/Tools/check_sources
--- a/Admin/lib/Tools/check_sources	Thu Mar 10 12:11:50 2016 +0100
+++ b/Admin/lib/Tools/check_sources	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Check_Sources "$@"
+isabelle java isabelle.Check_Sources "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/browser
--- a/lib/Tools/browser	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/browser	Thu Mar 10 17:30:04 2016 +0100
@@ -86,9 +86,9 @@
   esac
 
   if [ -z "$OUTFILE" ]; then
-    "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
+    isabelle java GraphBrowser.GraphBrowser "$(platform_path "$PRIVATE_FILE")"
   else
-    "$ISABELLE_TOOL" java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
+    isabelle java GraphBrowser.Console "$(platform_path "$PRIVATE_FILE")" "$(platform_path "$OUTFILE")"
   fi
   RC="$?"
 
@@ -102,7 +102,7 @@
   rm -f "$PRIVATE_FILE"
 elif [ -z "$ADMIN_BUILD" ]; then
   [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
-  exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+  exec isabelle java GraphBrowser.GraphBrowser
 else
   RC=0
 fi
diff -r cd266473b81b -r b5783412bfed lib/Tools/build
--- a/lib/Tools/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/build	Thu Mar 10 17:30:04 2016 +0100
@@ -169,7 +169,7 @@
 
 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
 
-"$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Build \
+isabelle java "${JAVA_ARGS[@]}" isabelle.Build \
   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
diff -r cd266473b81b -r b5783412bfed lib/Tools/console
--- a/lib/Tools/console	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/console	Thu Mar 10 17:30:04 2016 +0100
@@ -21,8 +21,8 @@
 
 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null
 then
-  exec "$ISABELLE_LINE_EDITOR" "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+  exec "$ISABELLE_LINE_EDITOR" isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
 else
   echo "### No line editor: \"$ISABELLE_LINE_EDITOR\""
-  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
+  exec isabelle java "${JAVA_ARGS[@]}" isabelle.ML_Console "$@"
 fi
diff -r cd266473b81b -r b5783412bfed lib/Tools/doc
--- a/lib/Tools/doc	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/doc	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Doc "$@"
+isabelle java isabelle.Doc "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/document
--- a/lib/Tools/document	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/document	Thu Mar 10 17:30:04 2016 +0100
@@ -128,12 +128,12 @@
     ./build "$OUTFORMAT" "$NAME"
     RC="$?"
   else
-    "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
-    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
-    { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \
-    { [ ! -f "$ROOT_NAME.idx" ] || "$ISABELLE_TOOL" latex -o idx "$ROOT_NAME.tex"; } && \
-    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
-    "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
+    isabelle latex -o sty "$ROOT_NAME.tex" && \
+    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+    { [ ! -f "$ROOT_NAME.bib" ] || isabelle latex -o bbl "$ROOT_NAME.tex"; } && \
+    { [ ! -f "$ROOT_NAME.idx" ] || isabelle latex -o idx "$ROOT_NAME.tex"; } && \
+    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
+    isabelle latex -o "$OUTFORMAT" "$ROOT_NAME.tex"
     RC="$?"
   fi
 
diff -r cd266473b81b -r b5783412bfed lib/Tools/options
--- a/lib/Tools/options	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/options	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-exec "$ISABELLE_TOOL" java isabelle.Options "$@"
+exec isabelle java isabelle.Options "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/process
--- a/lib/Tools/process	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/process	Thu Mar 10 17:30:04 2016 +0100
@@ -19,4 +19,4 @@
 
 mkdir -p "$ISABELLE_TMP_PREFIX" || exit $?
 
-"$ISABELLE_TOOL" java isabelle.ML_Process "$@"
+isabelle java isabelle.ML_Process "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/update_cartouches
--- a/lib/Tools/update_cartouches	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_cartouches	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Update_Cartouches "$@"
+isabelle java isabelle.Update_Cartouches "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/update_header
--- a/lib/Tools/update_header	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_header	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Update_Header "$@"
+isabelle java isabelle.Update_Header "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/update_then
--- a/lib/Tools/update_then	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_then	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Update_Then "$@"
+isabelle java isabelle.Update_Then "$@"
diff -r cd266473b81b -r b5783412bfed lib/Tools/update_theorems
--- a/lib/Tools/update_theorems	Thu Mar 10 12:11:50 2016 +0100
+++ b/lib/Tools/update_theorems	Thu Mar 10 17:30:04 2016 +0100
@@ -6,4 +6,4 @@
 
 isabelle_admin_build jars || exit $?
 
-"$ISABELLE_TOOL" java isabelle.Update_Theorems "$@"
+isabelle java isabelle.Update_Theorems "$@"
diff -r cd266473b81b -r b5783412bfed src/Doc/Classes/document/build
--- a/src/Doc/Classes/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Classes/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Codegen/document/build
--- a/src/Doc/Codegen/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Codegen/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -8,7 +8,7 @@
 # ad-hoc patching of temporary path from sources
 perl -i -pe 's/\{\\isachardollar\}ISABELLE\{\\isacharunderscore\}TMP\{\\isacharslash\}examples/examples/g' *.tex
 
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
 # clean up afterwards
diff -r cd266473b81b -r b5783412bfed src/Doc/Eisbach/document/build
--- a/src/Doc/Eisbach/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Eisbach/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo Eisbach
+isabelle logo Eisbach
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Implementation/document/build
--- a/src/Doc/Implementation/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Implementation/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Intro/document/build
--- a/src/Doc/Intro/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Intro/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo
+isabelle logo
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Isar_Ref/document/build
--- a/src/Doc/Isar_Ref/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Isar_Ref/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,7 +5,7 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo Isar
+isabelle logo Isar
 ./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/JEdit/document/build
--- a/src/Doc/JEdit/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/JEdit/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo jEdit
+isabelle logo jEdit
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Logics/document/build
--- a/src/Doc/Logics/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Logics/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo
+isabelle logo
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Logics_ZF/document/build
--- a/src/Doc/Logics_ZF/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Logics_ZF/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo ZF
+isabelle logo ZF
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Main/document/build
--- a/src/Doc/Main/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Main/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Nitpick/document/build
--- a/src/Doc/Nitpick/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Nitpick/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo Nitpick
+isabelle logo Nitpick
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Prog_Prove/document/build
--- a/src/Doc/Prog_Prove/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Prog_Prove/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo HOL
+isabelle logo HOL
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Sledgehammer/document/build
--- a/src/Doc/Sledgehammer/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Sledgehammer/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo -n isabelle_sledgehammer "S/H"
+isabelle logo -n isabelle_sledgehammer "S/H"
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/System/document/build
--- a/src/Doc/System/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/System/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,6 +5,6 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo
+isabelle logo
 "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/Doc/Tutorial/document/build
--- a/src/Doc/Tutorial/document/build	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/Tutorial/document/build	Thu Mar 10 17:30:04 2016 +0100
@@ -5,10 +5,10 @@
 FORMAT="$1"
 VARIANT="$2"
 
-"$ISABELLE_TOOL" logo HOL
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle logo HOL
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
 ./isa-index root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
diff -r cd266473b81b -r b5783412bfed src/Doc/prepare_document
--- a/src/Doc/prepare_document	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Doc/prepare_document	Thu Mar 10 17:30:04 2016 +0100
@@ -4,13 +4,13 @@
 
 FORMAT="$1"
 
-"$ISABELLE_TOOL" latex -o sty
+isabelle latex -o sty
 cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
 
-"$ISABELLE_TOOL" latex -o "$FORMAT"
-"$ISABELLE_TOOL" latex -o bbl
+isabelle latex -o "$FORMAT"
+isabelle latex -o bbl
 [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
 [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
-"$ISABELLE_TOOL" latex -o "$FORMAT"
+isabelle latex -o "$FORMAT"
 
diff -r cd266473b81b -r b5783412bfed src/HOL/Mirabelle/ex/Ex.thy
--- a/src/HOL/Mirabelle/ex/Ex.thy	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mirabelle/ex/Ex.thy	Thu Mar 10 17:30:04 2016 +0100
@@ -3,7 +3,7 @@
 
 ML {*
   val rc = Isabelle_System.bash
-    "cd \"$ISABELLE_HOME/src/HOL/Library\"; \"$ISABELLE_TOOL\" mirabelle arith Inner_Product.thy";
+    "cd \"$ISABELLE_HOME/src/HOL/Library\"; isabelle mirabelle arith Inner_Product.thy";
   if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
   else ();
 *} -- "some arbitrary small test case"
diff -r cd266473b81b -r b5783412bfed src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Thu Mar 10 17:30:04 2016 +0100
@@ -158,8 +158,8 @@
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $cmd =
-  "\"$ENV{'ISABELLE_TOOL'}\" process " .
-  "-o quick_and_dirty -o threads=1 -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
+  "isabelle process -o quick_and_dirty -o threads=1" .
+  " -e 'use_thy \"$path/$new_thy_name\"' $mirabelle_logic" . $quiet;
 my $result = system "bash", "-c", $cmd;
 
 if ($output_log) {
diff -r cd266473b81b -r b5783412bfed src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Thu Mar 10 17:30:04 2016 +0100
@@ -133,7 +133,7 @@
 
 # execution
 
-"$ISABELLE_TOOL" process -o auto_time_limit=10.0 \
+isabelle process -o auto_time_limit=10.0 \
   -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
 
 
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/CASC/ReadMe
--- a/src/HOL/TPTP/CASC/ReadMe	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/CASC/ReadMe	Thu Mar 10 17:30:04 2016 +0100
@@ -67,7 +67,7 @@
   year, because Isabelle now includes its own version of Java, but the solution
   back then was to replace
 
-  	exec "$ISABELLE_TOOL" java
+  	exec isabelle java
 
   in the last line of the "contrib/kodkodi-1.5.2/bin/kodkodi" script with
 
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_graph
--- a/src/HOL/TPTP/lib/Tools/tptp_graph	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Thu Mar 10 17:30:04 2016 +0100
@@ -118,7 +118,7 @@
 begin ML_file \"$TPTP_HOME/TPTP_Parser/tptp_to_dot.ML\" \
 ML {* TPTP_To_Dot.write_proof_dot \"$1\" \"$2\" *} end" \
         > $WORKDIR/$LOADER.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
+  isabelle process -e "use_thy \"$WORKDIR/$LOADER\";" Pure
 }
 
 function cleanup_workdir()
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.isabelle_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
 done
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_isabelle_hot
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle_hot	Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.isabelle_hot_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
 done
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_nitpick
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.nitpick_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
 done
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_refute
--- a/src/HOL/TPTP/lib/Tools/tptp_refute	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Thu Mar 10 17:30:04 2016 +0100
@@ -30,5 +30,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.refute_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
 done
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_sledgehammer
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Thu Mar 10 17:30:04 2016 +0100
@@ -31,5 +31,5 @@
   echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.sledgehammer_tptp_file @{theory} ($TIMEOUT) \"$FILE\" *} end" \
     > /tmp/$SCRATCH.thy
-  "$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+  isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
 done
diff -r cd266473b81b -r b5783412bfed src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Thu Mar 10 17:30:04 2016 +0100
@@ -28,4 +28,4 @@
 echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
 ML {* ATP_Problem_Import.translate_tptp_file @{theory} \"${args[0]}\" \"${args[1]}\" *} end" \
   > /tmp/$SCRATCH.thy
-"$ISABELLE_TOOL" process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
+isabelle process -e "use_thy \"/tmp/$SCRATCH\"; exit 1;" HOL-TPTP | grep --line-buffered -v "^###\|^PROOF FAILED for depth\|^Failure node\|inferences so far.  Searching to depth\|^val \|^Loading theory\|^Warning-The type of\|^   monotype.$"
diff -r cd266473b81b -r b5783412bfed src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Pure/Thy/present.ML	Thu Mar 10 17:30:04 2016 +0100
@@ -215,7 +215,7 @@
 
 fun isabelle_document {verbose, purge} format name tags dir =
   let
-    val s = "\"$ISABELLE_TOOL\" document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+    val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln s else ();
diff -r cd266473b81b -r b5783412bfed src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Mar 10 17:30:04 2016 +0100
@@ -209,7 +209,7 @@
 ## dependencies
 
 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
-  "$ISABELLE_TOOL" browser -b || exit $?
+  isabelle browser -b || exit $?
   "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
 fi
 
@@ -361,5 +361,5 @@
 then
   export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_PRINT_MODE JEDIT_BUILD_MODE
   classpath "$JEDIT_HOME/dist/jedit.jar"
-  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
+  exec isabelle java "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}"
 fi
diff -r cd266473b81b -r b5783412bfed src/Tools/jEdit/lib/Tools/jedit_client
--- a/src/Tools/jEdit/lib/Tools/jedit_client	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit_client	Thu Mar 10 17:30:04 2016 +0100
@@ -104,11 +104,11 @@
   exit
 fi
 
-"$ISABELLE_TOOL" jedit -b || exit $?
+isabelle jedit -b || exit $?
 
 if [ -f "$JEDIT_SETTINGS/$SERVER_NAME" ]
 then
-  exec "$ISABELLE_TOOL" java "${JAVA_ARGS[@]}" \
+  exec isabelle java "${JAVA_ARGS[@]}" \
     -jar $(platform_path "$JEDIT_HOME/dist/jedit.jar") \
     "-settings=$(platform_path "$JEDIT_SETTINGS")" \
     -server="$SERVER_NAME" -reuseview "${ARGS[@]}"
diff -r cd266473b81b -r b5783412bfed src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Thu Mar 10 12:11:50 2016 +0100
+++ b/src/Tools/jEdit/src/active.scala	Thu Mar 10 17:30:04 2016 +0100
@@ -33,7 +33,7 @@
                 Standard_Thread.fork("browser") {
                   val graph_file = Isabelle_System.tmp_file("graph")
                   File.write(graph_file, XML.content(body))
-                  Isabelle_System.bash("\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &",
+                  Isabelle_System.bash("isabelle browser -c \"$GRAPH_FILE\" &",
                     env = Map("GRAPH_FILE" -> File.standard_path(graph_file)))
                 }