diff --git a/thys/Huffman/ROOT b/thys/Huffman/ROOT
--- a/thys/Huffman/ROOT
+++ b/thys/Huffman/ROOT
@@ -1,117 +1,116 @@
 chapter AFP
 
 session Huffman (AFP) = HOL +
-  options [timeout = 600, document_preprocessor = "preprocessor"]
+  options [timeout = 600]
   theories 
     Huffman
   document_files
     "forest-a.eps"
     "forest-a.pdf"
     "forest-a.svg"
     "forest-flat.eps"
     "forest-flat.pdf"
     "forest-flat.svg"
     "forest-optimal.eps"
     "forest-optimal.pdf"
     "forest-optimal.svg"
     "forest-splitLeaf-ab.eps"
     "forest-splitLeaf-ab.pdf"
     "forest-splitLeaf-ab.svg"
     "forest-uniteTrees-flat.eps"
     "forest-uniteTrees-flat.pdf"
     "forest-uniteTrees-flat.svg"
     "forest-uniteTrees.eps"
     "forest-uniteTrees.pdf"
     "forest-uniteTrees.svg"
     "forest-zigzag.eps"
     "forest-zigzag.pdf"
     "forest-zigzag.svg"
-    "preprocessor"
     "root.tex"
     "tree-abc-full.eps"
     "tree-abc-full.pdf"
     "tree-abc-full.svg"
     "tree-abc-non-full.eps"
     "tree-abc-non-full.pdf"
     "tree-abc-non-full.svg"
     "tree-abcd-balanced-weighted.eps"
     "tree-abcd-balanced-weighted.pdf"
     "tree-abcd-balanced-weighted.svg"
     "tree-abcd-balanced.eps"
     "tree-abcd-balanced.pdf"
     "tree-abcd-balanced.svg"
     "tree-abcd-non-prefix.eps"
     "tree-abcd-non-prefix.pdf"
     "tree-abcd-non-prefix.svg"
     "tree-abcd-unbalanced-weighted.eps"
     "tree-abcd-unbalanced-weighted.pdf"
     "tree-abcd-unbalanced-weighted.svg"
     "tree-abcd-unbalanced.eps"
     "tree-abcd-unbalanced.pdf"
     "tree-abcd-unbalanced.svg"
     "tree-huffman-splitLeaf-ab.eps"
     "tree-huffman-splitLeaf-ab.pdf"
     "tree-huffman-splitLeaf-ab.svg"
     "tree-minima-abcd.eps"
     "tree-minima-abcd.pdf"
     "tree-minima-abcd.svg"
     "tree-minima.eps"
     "tree-minima.pdf"
     "tree-minima.svg"
     "tree-optimal.eps"
     "tree-optimal.pdf"
     "tree-optimal.svg"
     "tree-prime-step1.eps"
     "tree-prime-step1.pdf"
     "tree-prime-step1.svg"
     "tree-prime-step2.eps"
     "tree-prime-step2.pdf"
     "tree-prime-step2.svg"
     "tree-prime-step3.eps"
     "tree-prime-step3.pdf"
     "tree-prime-step3.svg"
     "tree-prime-step4.eps"
     "tree-prime-step4.pdf"
     "tree-prime-step4.svg"
     "tree-prime-step5.eps"
     "tree-prime-step5.pdf"
     "tree-prime-step5.svg"
     "tree-sibling.eps"
     "tree-sibling.pdf"
     "tree-sibling.svg"
     "tree-splitLeaf-a.eps"
     "tree-splitLeaf-a.pdf"
     "tree-splitLeaf-a.svg"
     "tree-splitLeaf-ab.eps"
     "tree-splitLeaf-ab.pdf"
     "tree-splitLeaf-ab.svg"
     "tree-splitLeaf-abcd-aba.eps"
     "tree-splitLeaf-abcd-aba.pdf"
     "tree-splitLeaf-abcd-aba.svg"
     "tree-splitLeaf-abcd.eps"
     "tree-splitLeaf-abcd.pdf"
     "tree-splitLeaf-abcd.svg"
     "tree-splitLeaf-ba.eps"
     "tree-splitLeaf-ba.pdf"
     "tree-splitLeaf-ba.svg"
     "tree-splitLeaf-cd.eps"
     "tree-splitLeaf-cd.pdf"
     "tree-splitLeaf-cd.svg"
     "tree-suboptimal.eps"
     "tree-suboptimal.pdf"
     "tree-suboptimal.svg"
     "tree-w1-plus-w2.eps"
     "tree-w1-plus-w2.pdf"
     "tree-w1-plus-w2.svg"
     "tree-w1-w2-leaves.eps"
     "tree-w1-w2-leaves.pdf"
     "tree-w1-w2-leaves.svg"
     "tree-w1-w2.eps"
     "tree-w1-w2.pdf"
     "tree-w1-w2.svg"
     "tree-w1.eps"
     "tree-w1.pdf"
     "tree-w1.svg"
     "tree-w2.eps"
     "tree-w2.pdf"
     "tree-w2.svg"
diff --git a/thys/Huffman/document/preprocessor b/thys/Huffman/document/preprocessor
deleted file mode 100755
--- a/thys/Huffman/document/preprocessor
+++ /dev/null
@@ -1,29 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-export HUFFMAN_TEX=Huffman.tex
-perl -pi -i.bak -e 's/\{\\isacharprime\}\{\\kern0pt\}a/\$\\alpha\$/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\{\\isacharprime\}\{\\kern0pt\}b/\$\\beta\$/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\{\\isacharbraceleft\}\{\\kern0pt\}\{\\isacharbraceright\}\{\\kern0pt\}/\{\\ensuremath\{\\emptyset\}\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\{\\isacharunderscore\}\{\\kern0pt\}\{\\isadigit\{([0-9])\}\}/\{\\isacharunderscore\}\{\1\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/([a-z]|\{\\isacharparenright\})\{\\isacharplus\}/\1\$\{\}^+\$/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\b(if|then|else(\\ if)?)\\( |isanewline)/\\ensuremath\{\\mathrm\{\1\}\}\\vthinspace\\\3/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\isactrlisub F/\\isactrlisub\{\\ensuremath\{\\mathsf\{\\scriptscriptstyle F\}\}\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/mergeSibling/merge\\-Sibling/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/swapFourSyms/swap\\-Four\\-Syms/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\{\\isasymSum\}(.*)\\ \{\\isasymin\}\\ (.*)\{\\isachardot\}/\\ensuremath\{\\sum_\{\1\\in\2\}\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\sum(.*)\\ \{\\isasymunion\}\\ /\\sum\1\\isasymunion/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\isacommand\{by\}/\\nopagebreak\\isacommand\{by\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/(\{assumes\})\\ /\1\\ \\ /g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/(\{shows\})\\ /\1\\ \\ /g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/(\\isachardoublequoteclose\})\\ (\{\\isachardoublequoteopen\})/\1\\ \\ \\,\2/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/(\{\\isacharparenright\}\{\\isachardoublequoteclose\}\\ )\\ \\,(\{\\isachardoublequoteopen\}\{\\isacharparenleft\})/\1\2/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\isactrlisub u\\isactrlisub *\{\\isacharprime\}/\\isactrlisub\{u\\isacharprime\}/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\isanewline$/%\
-\\isanewline/' $HUFFMAN_TEX
-sed '/\\isanewline$/,// s/^\(\(\\ \)*\)/\1\1/' $HUFFMAN_TEX > $HUFFMAN_TEX.bak
-mv $HUFFMAN_TEX.bak $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\{\\isacharcolon\}%/\{\\isacharcolon\}\\nopagebreak%/g' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/\\isakeyword\{where\}/\\isakeyword\{where\}\\nopagebreak/' $HUFFMAN_TEX
-perl -pi -i.bak -e 's/(\{\\isacharbrackleft\})(\{\\isacharbrackright\})/\1\\vthinspace\2/g' $HUFFMAN_TEX