--- a/src/HOL/TPTP/mash_eval.ML Thu Dec 19 10:15:12 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Thu Dec 19 13:43:21 2013 +0100
@@ -176,7 +176,7 @@
"slice" |> not slice ? prefix "dont_",
"type_enc = " ^ the_default "smart" type_enc,
"lam_trans = " ^ the_default "smart" lam_trans,
- "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
+ "timeout = " ^ ATP_Util.string_of_time timeout,
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val _ = print " * * *";
val _ = print ("Options: " ^ commas options);