lib/Tools/document

--- a/lib/Tools/document	Thu May 15 18:12:43 2008 +0200
+++ b/lib/Tools/document	Thu May 15 20:02:37 2008 +0200
@@ -139,10 +139,6 @@
   elif [ "$OUTFORMAT" = pdf ]; then
     pre_latex pdf && \
     "$ISATOOL" latex -o pdf && \
-    { if [ -n "$ISABELLE_THUMBPDF" ]; then
-        "$ISATOOL" latex -o png && \
-        "$ISATOOL" latex -o pdf
-      fi; }
     RC="$?"
   else
     pre_latex dvi && \