src/HOL/Tools/atp_wrapper.ML
changeset 30896 ec3f33437fe3
parent 30874 34927a1e0ae8
child 30899 d394a17d4fdb
     1.1 --- a/src/HOL/Tools/atp_wrapper.ML	Wed Apr 15 11:14:48 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Wed Apr 15 15:27:13 2009 +0200
     1.3 @@ -79,14 +79,16 @@
     1.4      val failure = find_failure proof
     1.5      val success = rc = 0 andalso is_none failure
     1.6      val message =
     1.7 -      if isSome failure then "Proof attempt failed."
     1.8 -      else if rc <> 0 then "Proof attempt failed: " ^ proof
     1.9 +      if is_some failure then "External prover failed."
    1.10 +      else if rc <> 0 then "External prover failed: " ^ proof
    1.11        else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
    1.12  
    1.13 -    val _ = if isSome failure
    1.14 +    val _ =
    1.15 +      if is_some failure
    1.16        then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
    1.17        else ()
    1.18 -    val _ = if rc <> 0
    1.19 +    val _ =
    1.20 +      if rc <> 0
    1.21        then Output.debug (fn () => "Sledgehammer exited with return code " ^ string_of_int rc ^ ":\n" ^ proof)
    1.22        else ()
    1.23    in (success, message) end;