1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Oct 04 07:01:22 2009 +0200
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Oct 04 11:45:41 2009 +0200
     1.3 @@ -299,7 +299,8 @@
     1.4  fun run_sh prover hard_timeout timeout dir st =
     1.5    let
     1.6      val (ctxt, goal) = Proof.get_goal st
     1.7 -    val ctxt' = ctxt |> is_some dir ? Config.put AtpWrapper.destdir (the dir)
     1.8 +    val ctxt' = if is_none dir then ctxt
     1.9 +      else Config.put AtpWrapper.destdir (the dir) ctxt
    1.10      val atp = prover (AtpWrapper.atp_problem_of_goal
    1.11        (AtpManager.get_full_types ()) 1 (ctxt', goal))
    1.12