# HG changeset patch
# User blanchet
# Date 1378763699 -7200
# Node ID c3d7d9911aae2786790792b500699f5cf7dfe1db
# Parent  2479b39d9d09ad2496fe04f932f5d4c044163056
since "full_proofs" can influence the proof search significantly (e.g. by disabling splitting for SPASS), it shouldn't be affected by the "debug" flag in the interest of minimizing confusion

diff -r 2479b39d9d09 -r c3d7d9911aae src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 09 23:09:37 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Sep 09 23:54:59 2013 +0200
@@ -839,8 +839,7 @@
             fun sel_weights () = atp_problem_selection_weights atp_problem
             fun ord_info () = atp_problem_term_order_info atp_problem
             val ord = effective_term_order ctxt name
-            val full_proof =
-              debug orelse (isar_proofs |> the_default (mode = Minimize))
+            val full_proof = isar_proofs |> the_default (mode = Minimize)
             val args =
               arguments ctxt full_proof extra
                         (slice_timeout |> the_default one_day)