1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 18:05:36 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 25 18:34:06 2010 +0200
     1.3 @@ -199,13 +199,10 @@
     1.4        0 => priority "No subgoal!"
     1.5      | n =>
     1.6        let
     1.7 -        val birth_time = Time.now ()
     1.8 -        val death_time = Time.+ (birth_time, timeout)
     1.9          val _ = kill_atps ()
    1.10          val _ = priority "Sledgehammering..."
    1.11 -        val _ = app (start_prover_thread params birth_time death_time i n
    1.12 -                                         relevance_override minimize_command
    1.13 -                                         state) atps
    1.14 +        val _ = app (start_prover_thread params i n relevance_override
    1.15 +                                         minimize_command state) atps
    1.16        in () end
    1.17  
    1.18  fun minimize override_params i refs state =