# HG changeset patch # User blanchet # Date 1402940381 -7200 # Node ID 49c1db0313e6283c54eeab3b7090ea800a5b9571 # Parent 8747af0d101291313d77dcd09ff0e068a7ae28ed give Z3 TPTP proofs a chance diff -r 8747af0d1012 -r 49c1db0313e6 src/HOL/Tools/ATP/atp_proof.ML --- 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) diff -r 8747af0d1012 -r 49c1db0313e6 src/HOL/Tools/ATP/atp_systems.ML --- 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,