# HG changeset patch
# User blanchet
# Date 1307721129 -7200
# Node ID 6f14d1386a1ebf2125bf78d6442c52ac7840bace
# Parent  2db277c6d506ab4cc6ee58019825bc8c53ba44bb
don't trim proofs in debug mode

diff -r 2db277c6d506 -r 6f14d1386a1e src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
@@ -652,9 +652,10 @@
                       type_sys true (Config.get ctxt atp_readable_names) true
                       hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
+                val full_proof = debug orelse isar_proof
                 val core =
                   File.shell_path command ^ " " ^
-                  arguments ctxt isar_proof slice slice_timeout weights ^ " " ^
+                  arguments ctxt full_proof slice slice_timeout weights ^ " " ^
                   File.shell_path prob_file
                 val command =
                   (if measure_run_time then