# HG changeset patch
# User boehmes
# Date 1254649541 -7200
# Node ID 5f1805c6ef2a64a2b8f75ade396f380864e5bb44
# Parent  6eafaa92a95ed9f238540e63b999f2671ccb3718
avoid exception Option: only apply "the" if needed

diff -r 6eafaa92a95e -r 5f1805c6ef2a src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Oct 04 07:01:22 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Oct 04 11:45:41 2009 +0200
@@ -299,7 +299,8 @@
 fun run_sh prover hard_timeout timeout dir st =
   let
     val (ctxt, goal) = Proof.get_goal st
-    val ctxt' = ctxt |> is_some dir ? Config.put AtpWrapper.destdir (the dir)
+    val ctxt' = if is_none dir then ctxt
+      else Config.put AtpWrapper.destdir (the dir) ctxt
     val atp = prover (AtpWrapper.atp_problem_of_goal
       (AtpManager.get_full_types ()) 1 (ctxt', goal))