--- a/src/HOL/TPTP/TPTP_Parser/make_mlyacclib Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib Tue Mar 25 19:03:02 2014 +0100
@@ -20,8 +20,6 @@
(* 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:
@@ -48,7 +46,6 @@
cat <<EOF
;
-print_depth 10;
EOF
) > ml_yacc_lib.ML
\ No newline at end of file