# HG changeset patch
# User blanchet
# Date 1290687972 -3600
# Node ID a4171afcc3c49a896f029164cc7e1cad6557fbb8
# Parent  7fa054c3f810b4c0d443ca79e0312260a06800a1
set Metis option on correct context, lest it be ignored

diff -r 7fa054c3f810 -r a4171afcc3c4 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 12:11:12 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Nov 25 13:26:12 2010 +0100
@@ -516,16 +516,16 @@
 
 val smt_metis_timeout = seconds 0.5
 
-fun can_apply_metis state i ths =
-  can_apply smt_metis_timeout (fn ctxt => Metis_Tactics.metis_tac ctxt ths)
-            state i
+fun can_apply_metis debug state i ths =
+  can_apply smt_metis_timeout
+            (Config.put Metis_Tactics.verbose debug
+             #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths)) state i
 
 fun run_smt_solver auto remote (params as {debug, ...}) minimize_command
         ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let
     val repair_context =
-      Config.put Metis_Tactics.verbose debug
-      #> Config.put SMT_Config.verbose debug
+      Config.put SMT_Config.verbose debug
       #> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
     val state = state |> Proof.map_context repair_context
     val thy = Proof.theory_of state
@@ -538,8 +538,10 @@
         NONE =>
         let
           val method =
-            if can_apply_metis state subgoal (map snd used_facts) then "metis"
-            else "smt"
+            if can_apply_metis debug state subgoal (map snd used_facts) then
+              "metis"
+            else
+              "smt"
         in
           try_command_line (proof_banner auto)
                            (apply_on_subgoal subgoal subgoal_count ^