src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 43354 396aaa15dd8b
parent 43304 6901ebafbb8d
child 43360 6f14d1386a1e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 12:01:15 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -654,7 +654,7 @@
     1.4                  fun weights () = atp_problem_weights atp_problem
     1.5                  val core =
     1.6                    File.shell_path command ^ " " ^
     1.7 -                  arguments ctxt slice slice_timeout weights ^ " " ^
     1.8 +                  arguments ctxt isar_proof slice slice_timeout weights ^ " " ^
     1.9                    File.shell_path prob_file
    1.10                  val command =
    1.11                    (if measure_run_time then