--- 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"