1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Oct 04 11:28:28 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Oct 04 11:12:28 2013 +0200
     1.3 @@ -309,20 +309,21 @@
     1.4  
     1.5        val launch_ueq_atps = launch_atps "Unit-equational provers" (SOME is_unit_equality) ueq_atps
     1.6  
     1.7 -      fun launch_atps_and_smt_solvers () =
     1.8 +      fun launch_atps_and_smt_solvers p =
     1.9          [launch_full_atps, launch_smts, launch_ueq_atps]
    1.10 -        |> Par_List.map (fn f => ignore (f (unknownN, state)))
    1.11 +        |> Par_List.map (fn f => fst (f p))
    1.12          handle ERROR msg => (print ("Error: " ^ msg); error msg)
    1.13  
    1.14        fun maybe f (accum as (outcome_code, _)) =
    1.15          accum |> (mode = Normal orelse outcome_code <> someN) ? f
    1.16      in
    1.17        (unknownN, state)
    1.18 -      |> (if blocking then
    1.19 +      |> (if mode = Auto_Try then
    1.20              launch_full_atps
    1.21 -            #> mode <> Auto_Try ? (maybe launch_ueq_atps #> maybe launch_smts)
    1.22 +          else if blocking then
    1.23 +            launch_atps_and_smt_solvers #> max_outcome_code #> rpair state
    1.24            else
    1.25 -            (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
    1.26 +            (fn p => (Future.fork (tap (fn () => launch_atps_and_smt_solvers p)); p)))
    1.27        handle TimeLimit.TimeOut =>
    1.28               (print "Sledgehammer ran out of time."; (unknownN, state))
    1.29      end