# HG changeset patch # User huffman # Date 1235150123 28800 # Node ID 80db6f3c523ef969c24179746371fa6e8e017200 # Parent a2f19e0a28b25c63524f52b5a753ac9e166ab969# Parent d8b6542e643f2f0160620860ead211fa0ae22c64 merged diff -r a2f19e0a28b2 -r 80db6f3c523e src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Fri Feb 20 08:02:11 2009 -0800 +++ b/src/HOL/Tools/atp_wrapper.ML Fri Feb 20 09:15:23 2009 -0800 @@ -78,10 +78,14 @@ val failure = find_failure proof val success = rc = 0 andalso is_none failure val message = - if isSome failure then "Could not prove: " ^ the failure - else if rc <> 0 - then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof - else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) + if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) + else "Could not prove goal." + val _ = if isSome failure + then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) + else () + val _ = if rc <> 0 + then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof) + else () in (success, message) end;