--- 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)