# HG changeset patch
# User blanchet
# Date 1335357201 -7200
# Node ID df437d1bf8db90dff6da070ab00595ce1433e188
# Parent  11b4395aaf0ce7dac07cc4f6dafbd0bcea57883c
tweak TPTP Nitpick's output

diff -r 11b4395aaf0c -r df437d1bf8db src/HOL/TPTP/atp_problem_import.ML
--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 14:33:21 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 14:33:21 2012 +0200
@@ -73,11 +73,13 @@
        ("max_threads", "1"),
        ("batch_size", "10"),
        ("falsify", if null conjs then "false" else "true"),
-       (* ("debug", "true"), *)
        ("verbose", "true"),
-       (* ("overlord", "true"), *)
+(*
+       ("debug", "true"),
+       ("overlord", "true"),
+*)
        ("show_consts", "true"),
-       ("format", "1000"),
+       ("format", "1"),
        ("max_potential", "0"),
        ("timeout", string_of_int timeout),
        ("tac_timeout", string_of_int ((timeout + 49) div 50))]