diff -r 8d5d255bf89c -r 5d9aab0c609c src/HOL/TPTP/TPTP_Parser/make_tptp_parser
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/make_tptp_parser	Fri Mar 09 15:38:55 2012 +0000
@@ -0,0 +1,84 @@
+#!/bin/bash
+#
+# make_tptp_parser - Generates Isabelle-friendly version of ML-Yacc's library,
+#                    runs ML-Yacc to generate TPTP parser, and makes the
+#                    generated parser Isabelle-friendly.
+#
+# This code is based on that used in src/Tools/Metis to adapt Metis for
+# use in Isabelle.
+
+MLYACCDIR=./ml-yacc
+INTERMEDIATE_FILES="tptp.yacc.sig tptp.lex.sml tptp.yacc.sml"
+MLYACCLIB_FILES="base.sig join.sml lrtable.sml stream.sml parser2.sml"
+
+echo "Cleaning"
+rm -f {tptp_lexyacc,ml_yacc_lib}.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;' $FILE
+done
+) > tptp_lexyacc.ML
+
+rm -f $INTERMEDIATE_FILES tptp.yacc.desc
+
+#Now patch and collate ML-Yacc's library files
+echo "Generating ml_yacc_lib.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 *)
+(******************************************************************)
+
+print_depth 0;
+
+(*
+  This file is generated from the contents of ML-Yacc's lib directory.
+  ML-Yacc's COPYRIGHT-file contents follow:
+
+EOF
+  perl -pe 'print "  ";' ml-yacc/COPYRIGHT
+  echo "*)"
+
+for FILE in $MLYACCLIB_FILES
+do
+  echo
+  echo "(**** Original file: $FILE ****)"
+  echo
+  echo -e "  $FILE" >&2
+  perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \
+          -e 's/Unsafe\.(.*)/\1/g;' \
+          -e 's/\bconcat\b/String.concat/g;' \
+          -e 's/(?<!List\.)foldr\b/List.foldr/g;' \
+          -e 's/\bfoldl\b/List.foldl/g;' \
+          -e 's/val print = fn s => TextIO\.output\(TextIO\.stdOut,s\)$//g;' \
+          -e 's/\bprint\b/TextIO.print/g;' \
+          $MLYACCDIR/lib/$FILE
+  done
+
+  cat <<EOF
+;
+print_depth 10;
+EOF
+
+) > ml_yacc_lib.ML
\ No newline at end of file