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