# HG changeset patch
# User blanchet
# Date 1284193497 -7200
# Node ID 23951979a362b6e35a949329c979fcc120dd0ce8
# Parent  5d578004be23aebabf0a2cea31b97a2eed65c67b
make Mirabelle happy

diff -r 5d578004be23 -r 23951979a362 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 11 10:24:13 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Sep 11 10:24:57 2010 +0200
@@ -304,11 +304,12 @@
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val thy = ProofContext.theory_of ctxt
     val i = 1
-    val change_dir = (fn SOME d => Config.put Sledgehammer.dest_dir d | _ => I)
-    val ctxt' =
-      ctxt
-      |> change_dir dir
-      |> Config.put Sledgehammer.measure_run_time true
+    fun change_dir (SOME dir) = Config.put Sledgehammer.dest_dir dir
+      | change_dir NONE = I
+    val st' =
+      st |> Proof.map_context
+                (change_dir dir
+                 #> Config.put Sledgehammer.measure_run_time true)
     val params as {full_types, relevance_thresholds, max_relevant, ...} =
       Sledgehammer_Isar.default_params thy
           [("timeout", Int.toString timeout ^ " s")]
@@ -320,7 +321,7 @@
           (the_default default_max_relevant max_relevant)
           relevance_override chained_ths hyp_ts concl_t
     val problem =
-      {ctxt = ctxt', goal = goal, subgoal = i,
+      {state = st', goal = goal, subgoal = i,
        axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
     val time_limit =
       (case hard_timeout of