src/HOL/Tools/atp_wrapper.ML
changeset 30016 76b58a07e704
parent 30015 1baeda435aa6
child 30151 629f3a92863e
equal deleted inserted replaced
30015:1baeda435aa6 30016:76b58a07e704
    77     (* check for success and print out some information on failure *)
    77     (* check for success and print out some information on failure *)
    78     val failure = find_failure proof
    78     val failure = find_failure proof
    79     val success = rc = 0 andalso is_none failure
    79     val success = rc = 0 andalso is_none failure
    80     val message =
    80     val message =
    81       if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
    81       if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
    82       else "Could not prove."
    82       else "Could not prove goal."
    83     val _ = if isSome failure
    83     val _ = if isSome failure
    84       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
    84       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
    85       else ()
    85       else ()
    86     val _ = if rc <> 0
    86     val _ = if rc <> 0
    87       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
    87       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)