diff --git a/src/Doc/Tutorial/document/build b/src/Doc/Tutorial/document/build
--- a/src/Doc/Tutorial/document/build
+++ b/src/Doc/Tutorial/document/build
@@ -1,13 +1,12 @@
 #!/usr/bin/env bash
 
 set -e
 
 FORMAT="$1"
 VARIANT="$2"
 
 isabelle latex -o "$FORMAT"
 isabelle latex -o bbl
 ./isa-index root
 isabelle latex -o "$FORMAT"
-[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
 isabelle latex -o "$FORMAT"
diff --git a/src/Doc/fixbookmarks b/src/Doc/fixbookmarks
deleted file mode 100755
--- a/src/Doc/fixbookmarks
+++ /dev/null
@@ -1,3 +0,0 @@
-#!/usr/bin/env bash
-
-perl -pi -e 's/\\([a-zA-Z]+)\s*/$1/g; s/\$//g; s/^BOOKMARK/\\BOOKMARK/g;' "$@"
diff --git a/src/Doc/prepare_document b/src/Doc/prepare_document
--- a/src/Doc/prepare_document
+++ b/src/Doc/prepare_document
@@ -1,12 +1,11 @@
 #!/usr/bin/env bash
 
 set -e
 
 FORMAT="$1"
 
 isabelle latex -o "$FORMAT"
 isabelle latex -o bbl
 [ -f root.idx ] && "$ISABELLE_HOME/src/Doc/sedindex" root
 isabelle latex -o "$FORMAT"
-[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
 isabelle latex -o "$FORMAT"