--- a/src/HOL/TPTP/mash_eval.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Thu May 16 13:34:13 2013 +0200
@@ -75,7 +75,7 @@
let val facts = facts |> map (fst o fst) in
str_of_method method ^
(if is_none outcome then
- "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
+ "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
(used_facts |> map (with_index facts o fst)
|> sort (int_ord o pairself fst)
|> map index_str
@@ -199,7 +199,7 @@
"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),
+ "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val _ = print " * * *";
val _ = print ("Options: " ^ commas options);