changeset 62015 | db9c2af6ce72 |
parent 53498 | 05313b45a5ae |
--- 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