src/HOL/TPTP/TPTP_Parser/make_tptp_parser

replaced some lemmas' implicit formulas by explicit ones to avoid silent changes

#!/usr/bin/env bash
#
# make_tptp_parser - Runs ML-Yacc to generate TPTP parser and makes it
#                    Isabelle-friendly.
#
# This code is based on that used in src/Tools/Metis to adapt Metis for
# use in Isabelle.

INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"

echo "Cleaning"
rm -f tptp_lexyacc.ML
echo "Generating lexer and parser"
ml-lex tptp.lex && ml-yacc tptp.yacc
echo "Generating tptp_lexyacc.ML"
(
  cat <<EOF

(******************************************************************)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)

(*
  This file is produced from the parser generated by ML-Yacc from the
  source files tptp.lex and tptp.yacc.
*)
EOF

for FILE in $INTERMEDIATE_FILES
do
  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
          -e 's/Unsafe\.(.*)/\1/g;' \
          -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE
done
) | expand -t8 > tptp_lexyacc.ML

rm -f $INTERMEDIATE_FILES tptp.yacc.desc