author | immler@in.tum.de |
Fri, 20 Feb 2009 16:48:01 +0100 | |
changeset 30016 | 76b58a07e704 |
parent 30015 | 1baeda435aa6 |
child 30017 | d8b6542e643f |
--- a/src/HOL/Tools/atp_wrapper.ML Fri Feb 20 11:04:18 2009 +0100 +++ b/src/HOL/Tools/atp_wrapper.ML Fri Feb 20 16:48:01 2009 +0100 @@ -79,7 +79,7 @@ val success = rc = 0 andalso is_none failure val message = if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) - else "Could not prove." + else "Could not prove goal." val _ = if isSome failure then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof) else ()