changeset 53586 | bd5fa6425993 |
parent 52995 | ab98feb66684 |
child 53980 | 7e6a82c593f4 |
--- a/src/HOL/TPTP/atp_theory_export.ML Thu Sep 12 20:54:26 2013 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Thu Sep 12 22:10:57 2013 +0200 @@ -71,7 +71,7 @@ tracing ("Ran ATP: " ^ (case outcome of NONE => "Success" - | SOME failure => string_of_failure failure)) + | SOME failure => string_of_atp_failure failure)) in outcome end fun is_problem_line_reprovable ctxt format prelude axioms deps