--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 13:17:37 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Oct 26 13:50:57 2010 +0200
@@ -316,11 +316,10 @@
fun get_prover ctxt args =
let
- val thy = ProofContext.theory_of ctxt
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
- fun get_prover name = (name, Sledgehammer.get_prover thy false name)
+ fun get_prover name = (name, Sledgehammer.get_prover ctxt false name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name