diff -r 7edd43d0c0ba -r 16696e649fea src/HOL/TPTP/lib/Tools/tptp_graph
--- a/src/HOL/TPTP/lib/Tools/tptp_graph	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_graph	Tue Sep 03 21:46:40 2013 +0100
@@ -143,8 +143,8 @@
 cd $WORKDIR
 if [ -z "$NON_EXEC" ]; then
   $DOT -Txdot "${FILENAME}.dot" \
-  | $DOT2TEX -f pgf -t raw --crop > "${FILENAME}.tex"
-  $PERL -w -p -e 's/_/\\_/g' "${FILENAME}.tex"
+  | $DOT2TEX -f pgf -t raw --crop \
+  | $PERL -w -p -e 's/_/\\_/g' > "${FILENAME}.tex"
 fi
 
 if [ "$OUTPUT_FORMAT" -eq 1 ]; then