# HG changeset patch
# User wenzelm
# Date 1357668132 -3600
# Node ID 5a9964f7a6915cfa8a144fc9acc9fddec562ff9b
# Parent  26ad3da13f47c1a1d301a7c02a73fcb03aaa1f74# Parent  8c1cda8ad83306a2bca6533052a8af07b4122bdb
merged

diff -r 8c1cda8ad833 -r 5a9964f7a691 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Tue Jan 08 18:24:52 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Tue Jan 08 19:02:12 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);