diff -r 446fcbadc6bf -r db9c2af6ce72 src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- a/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Thu Dec 31 20:40:28 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Thu Dec 31 20:57:00 2015 +0100
@@ -34,6 +34,6 @@
           -e 's/Unsafe\.(.*)/\1/g;' \
           -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
 done
-) > tptp_lexyacc.ML
+) | expand -t8 > tptp_lexyacc.ML
 
 rm -f $INTERMEDIATE_FILES tptp.yacc.desc