--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 15:01:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Tue Oct 26 16:56:54 2010 +0200
@@ -92,8 +92,7 @@
state axioms =
let
val thy = Proof.theory_of state
- val ctxt = Proof.context_of state
- val prover = get_prover ctxt false prover_name
+ val prover = get_prover thy false prover_name
val msecs = Time.toMilliseconds timeout
val _ = Output.urgent_message ("Sledgehammer minimize: " ^ quote prover_name ^ ".")
val {goal, ...} = Proof.goal state