src/HOL/Tools/atp_wrapper.ML
changeset 30015 1baeda435aa6
parent 29597 0f4f36779ca7
child 30016 76b58a07e704
equal deleted inserted replaced
30001:dd27e16677b2 30015:1baeda435aa6
    76     
    76     
    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 isSome failure then "Could not prove: " ^ the failure
    81       if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
    82       else if rc <> 0
    82       else "Could not prove."
    83       then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof 
    83     val _ = if isSome failure
    84       else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
    84       then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
       
    85       else ()
       
    86     val _ = if rc <> 0
       
    87       then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
       
    88       else ()
    85   in (success, message) end;
    89   in (success, message) end;
    86 
    90 
    87 
    91 
    88 
    92 
    89 (** common provers **)
    93 (** common provers **)