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"