# HG changeset patch
# User blanchet
# Date 1357647399 -3600
# Node ID 26ad3da13f47c1a1d301a7c02a73fcb03aaa1f74
# Parent  d5c07ddd929be1e6a425f1263ee9690753a747e5
tuned output

diff -r d5c07ddd929b -r 26ad3da13f47 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Tue Jan 08 10:34:19 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Jan 08 13:16:39 2013 +0100
@@ -137,10 +137,12 @@
                (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
-      [prover, string_of_int (the max_facts) ^ " facts",
-       "slice" |> not slice ? prefix "dont_", the_default "smart" type_enc,
-       the_default "smart" lam_trans,
-       ATP_Util.string_from_time (timeout |> the_default one_year),
+      ["prover = " ^ prover,
+       "max_facts = " ^ string_of_int (the max_facts),
+       "slice" |> not slice ? prefix "dont_",
+       "type_enc = " ^ the_default "smart" type_enc,
+       "lam_trans = " ^ the_default "smart" lam_trans,
+       "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout),
        "instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
     val _ = print " * * *";
     val _ = print ("Options: " ^ commas options);