# HG changeset patch
# User blanchet
# Date 1315608265 -7200
# Node ID d615dfa8857220f9e23a17821288f6e9af2a63a0
# Parent  73d5b722c4b4999c162824864131eb050ba79f1e
continue with minimization in debug mode in spite of unsoundness

diff -r 73d5b722c4b4 -r d615dfa88572 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Sep 09 09:31:04 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sat Sep 10 00:44:25 2011 +0200
@@ -690,14 +690,22 @@
                 val outcome =
                   case outcome of
                     NONE =>
-                    used_facts_in_unsound_atp_proof ctxt
-                        conjecture_shape facts_offset fact_names atp_proof
-                    |> Option.map (fn facts =>
-                           UnsoundProof
-                               (if is_type_enc_quasi_sound type_enc then
-                                  SOME sound
-                                else
-                                  NONE, facts |> sort string_ord))
+                    (case used_facts_in_unsound_atp_proof ctxt
+                              conjecture_shape facts_offset fact_names atp_proof
+                          |> Option.map (sort string_ord) of
+                       SOME facts =>
+                       let
+                         val failure =
+                           (if is_type_enc_quasi_sound type_enc then SOME sound
+                            else NONE, facts)
+                           |> UnsoundProof
+                       in
+                         if debug then
+                           (warning (string_for_failure failure); NONE)
+                         else
+                           SOME failure
+                       end
+                     | NONE => NONE)
                   | _ => outcome
               in
                 ((pool, conjecture_shape, facts_offset, fact_names,