# HG changeset patch
# User immler@in.tum.de
# Date 1244041001 -7200
# Node ID 1d00ab68bc8d337c7eecddac0828868d3c252493
# Parent  c231efe693ce95b999da60c0e6f07c1a2eaec3d5
additional debugging

diff -r c231efe693ce -r 1d00ab68bc8d src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jun 03 16:56:41 2009 +0200
@@ -93,15 +93,7 @@
       if is_some failure then "External prover failed."
       else if rc <> 0 then "External prover failed: " ^ proof
       else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
-
-    val _ =
-      if is_some 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 ()
+    val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
   in (success, message, proof, thm_names, the_const_counts) end;