1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:08:50 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 04 15:09:37 2010 +0200
     1.3 @@ -226,7 +226,7 @@
     1.4        let
     1.5          val birth_time = Time.now ()
     1.6          val death_time = Time.+ (birth_time, timeout)
     1.7 -        val _ = kill_atps ()  (* race w.r.t. other Sledgehammer invocations *)
     1.8 +        val _ = kill_atps ()
     1.9          val _ = priority "Sledgehammering..."
    1.10          val _ = app (start_prover_thread params birth_time death_time i n
    1.11                                           relevance_override minimize_command
    1.12 @@ -249,8 +249,10 @@
    1.13    in
    1.14      case subgoal_count state of
    1.15        0 => priority "No subgoal!"
    1.16 -    | n => priority (#2 (minimize_theorems (get_params thy override_params) i n
    1.17 -                                           state name_thms_pairs))
    1.18 +    | n =>
    1.19 +      (kill_atps ();
    1.20 +       priority (#2 (minimize_theorems (get_params thy override_params) i n
    1.21 +                                       state name_thms_pairs)))
    1.22    end
    1.23  
    1.24  val sledgehammerN = "sledgehammer"