# HG changeset patch
# User blanchet
# Date 1292508737 -3600
# Node ID b16fbb148a16b194bc5172da203732790cf0e4b9
# Parent  209546e0af2c8236979fd0efed9fed6c09bc17ef
tuning

diff -r 209546e0af2c -r b16fbb148a16 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 16 15:12:17 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 16 15:12:17 2010 +0100
@@ -346,7 +346,6 @@
 fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
-    val thy = ProofContext.theory_of ctxt
     val i = 1
     fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
       | change_dir NONE = I
@@ -538,8 +537,6 @@
       val named_thms =
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
       val ctxt = Proof.context_of pre
-      val (prover_name, _) = get_prover ctxt args
-      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
       val trivial =