--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 19:18:10 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 19:39:41 2014 +0200
@@ -706,7 +706,7 @@
map map_step
end
-fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
+fun nasty_name pool s = Symtab.lookup pool s |> the_default s
fun nasty_atp_proof pool =
not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool)
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:18:10 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Jun 16 19:39:41 2014 +0200
@@ -576,7 +576,7 @@
val z3_tptp_config : atp_config =
{exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
- "-core -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
+ "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
proof_delims = [("SZS status Theorem", "")],
known_failures = known_szs_status_failures,
prem_role = Hypothesis,