don't trim proofs in debug mode
authorblanchet
Fri Jun 10 17:52:09 2011 +0200 (2011-06-10)
changeset 433606f14d1386a1e
parent 43359 2db277c6d506
child 43361 e37b54d429f5
don't trim proofs in debug mode
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 17:52:09 2011 +0200
     1.3 @@ -652,9 +652,10 @@
     1.4                        type_sys true (Config.get ctxt atp_readable_names) true
     1.5                        hyp_ts concl_t facts
     1.6                  fun weights () = atp_problem_weights atp_problem
     1.7 +                val full_proof = debug orelse isar_proof
     1.8                  val core =
     1.9                    File.shell_path command ^ " " ^
    1.10 -                  arguments ctxt isar_proof slice slice_timeout weights ^ " " ^
    1.11 +                  arguments ctxt full_proof slice slice_timeout weights ^ " " ^
    1.12                    File.shell_path prob_file
    1.13                  val command =
    1.14                    (if measure_run_time then