--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri May 27 10:30:07 2011 +0200
@@ -479,7 +479,7 @@
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
- val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
+ val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
val (dest_dir, problem_prefix) =
if overlord then overlord_file_location_for_prover name
else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix)