avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures

--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -231,7 +231,6 @@
         val _ = Proof.assert_backward state
         val print =
           if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
-        val state = state |> Proof.map_context (silence_proof_methods debug)
         val ctxt = Proof.context_of state
         val {facts = chained, goal, ...} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -290,7 +290,7 @@
         val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
         val _ = fold_isar_steps (fn meth =>
-            K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth []))
+            K (set_preplay_outcomes_of_isar_step ctxt debug preplay_timeout preplay_data meth []))
           (steps_of_isar_proof canonical_isar_proof) ()
 
         fun str_of_preplay_outcome outcome =
@@ -316,11 +316,11 @@
         val (play_outcome, isar_proof) =
           canonical_isar_proof
           |> tap (trace_isar_proof "Original")
-          |> compress_isar_proof ctxt compress_isar preplay_timeout preplay_data
+          |> compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data
           |> tap (trace_isar_proof "Compressed")
           |> postprocess_isar_proof_remove_unreferenced_steps
                (keep_fastest_method_of_isar_step (!preplay_data)
-                #> minimize ? minimize_isar_step_dependencies ctxt preplay_data)
+                #> minimize ? minimize_isar_step_dependencies ctxt debug preplay_data)
           |> tap (trace_isar_proof "Minimized")
           (* It's not clear whether this is worth the trouble (and if so, "isar_compress" has an
              unnatural semantics): *)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -11,7 +11,7 @@
   type isar_proof = Sledgehammer_Isar_Proof.isar_proof
   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
 
-  val compress_isar_proof : Proof.context -> real -> Time.time ->
+  val compress_isar_proof : Proof.context -> bool -> real -> Time.time ->
     isar_preplay_data Unsynchronized.ref -> isar_proof -> isar_proof
 end;
 
@@ -109,7 +109,7 @@
 val compress_degree = 2
 
 (* Precondition: The proof must be labeled canonically. *)
-fun compress_isar_proof ctxt compress_isar preplay_timeout preplay_data proof =
+fun compress_isar_proof ctxt debug compress_isar preplay_timeout preplay_data proof =
   if compress_isar <= 1.0 then
     proof
   else
@@ -172,11 +172,12 @@
               (* check if the modified step can be preplayed fast enough *)
               val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
             in
-              (case preplay_isar_step ctxt timeout hopeless step'' of
+              (case preplay_isar_step ctxt debug timeout hopeless step'' of
                 meths_outcomes as (_, Played time'') :: _ =>
                 (* l' successfully eliminated *)
                 (decrement_step_count ();
-                 set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step'' meths_outcomes;
+                 set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step''
+                   meths_outcomes;
                  map (replace_successor l' [l]) lfs';
                  elim_one_subproof time'' step'' subs nontriv_subs)
               | _ => elim_one_subproof time step subs (sub :: nontriv_subs))
@@ -215,14 +216,16 @@
                   val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
                   val timeouts =
                     map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
-                  val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
+                  val meths_outcomess =
+                    map3 (preplay_isar_step ctxt debug) timeouts hopelesses succs'
                 in
                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
                     NONE => steps
                   | SOME times =>
                     (* candidate successfully eliminated *)
                     (decrement_step_count ();
-                     map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
+                     map3 (fn time =>
+                         set_preplay_outcomes_of_isar_step ctxt debug time preplay_data)
                        times succs' meths_outcomess;
                      map (replace_successor l labels) lfs;
                      steps_before @ update_steps succs' steps_after))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -12,8 +12,8 @@
   type isar_preplay_data = Sledgehammer_Isar_Preplay.isar_preplay_data
 
   val keep_fastest_method_of_isar_step : isar_preplay_data -> isar_step -> isar_step
-  val minimize_isar_step_dependencies : Proof.context -> isar_preplay_data Unsynchronized.ref ->
-    isar_step -> isar_step
+  val minimize_isar_step_dependencies : Proof.context -> bool ->
+    isar_preplay_data Unsynchronized.ref -> isar_step -> isar_step
   val postprocess_isar_proof_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof ->
     isar_proof
 end;
@@ -34,7 +34,7 @@
 
 val slack = seconds 0.025
 
-fun minimize_isar_step_dependencies ctxt preplay_data
+fun minimize_isar_step_dependencies ctxt debug preplay_data
       (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs0), meths as meth :: _, comment)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
@@ -43,7 +43,7 @@
 
         fun minimize_facts _ min_facts [] time = (min_facts, time)
           | minimize_facts mk_step min_facts (fact :: facts) time =
-            (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
+            (case preplay_isar_step_for_method ctxt debug (Time.+ (time, slack)) meth
                 (mk_step (min_facts @ facts)) of
               Played time' => minimize_facts mk_step min_facts facts time'
             | _ => minimize_facts mk_step (fact :: min_facts) facts time)
@@ -53,11 +53,12 @@
 
         val step' = mk_step_lfs_gfs min_lfs min_gfs
       in
-        set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')];
+        set_preplay_outcomes_of_isar_step ctxt debug time'' preplay_data step'
+          [(meth, Played time'')];
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))
-  | minimize_isar_step_dependencies _ _ step = step
+  | minimize_isar_step_dependencies _ _ _ step = step
 
 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
   let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -18,11 +18,11 @@
   type isar_preplay_data
 
   val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
-  val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
-    play_outcome
-  val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
+  val preplay_isar_step_for_method : Proof.context -> bool -> Time.time -> proof_method ->
+    isar_step -> play_outcome
+  val preplay_isar_step : Proof.context -> bool -> Time.time -> proof_method list -> isar_step ->
     (proof_method * play_outcome) list
-  val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
+  val set_preplay_outcomes_of_isar_step : Proof.context -> bool -> Time.time ->
     isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
   val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
   val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
@@ -101,7 +101,8 @@
   end
 
 (* may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+fun raw_preplay_step_for_method ctxt debug timeout meth
+    (Prove (_, xs, _, t, subproofs, facts, _, _)) =
   let
     val goal =
       (case xs of
@@ -128,7 +129,7 @@
 
     fun prove () =
       Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
-        HEADGOAL (tac_of_proof_method ctxt assmsp meth))
+        HEADGOAL (tac_of_proof_method ctxt debug assmsp meth))
       handle ERROR msg => error ("Preplay error: " ^ msg)
 
     val play_outcome = take_time timeout prove ()
@@ -137,13 +138,13 @@
     play_outcome
   end
 
-fun preplay_isar_step_for_method ctxt timeout meth =
-  try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt debug timeout meth =
+  try (raw_preplay_step_for_method ctxt debug timeout meth) #> the_default Play_Failed
 
-fun preplay_isar_step ctxt timeout hopeless step =
+fun preplay_isar_step ctxt debug timeout hopeless step =
   let
     fun try_method meth =
-      (case preplay_isar_step_for_method ctxt timeout meth step of
+      (case preplay_isar_step_for_method ctxt debug timeout meth step of
         outcome as Played _ => SOME (meth, outcome)
       | _ => NONE)
 
@@ -163,11 +164,11 @@
   | add_preplay_outcomes play1 play2 =
     Play_Timed_Out (Time.+ (pairself time_of_play (play1, play2)))
 
-fun set_preplay_outcomes_of_isar_step ctxt timeout preplay_data
+fun set_preplay_outcomes_of_isar_step ctxt debug timeout preplay_data
       (step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
     let
       fun lazy_preplay meth =
-        Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+        Lazy.lazy (fn () => preplay_isar_step_for_method ctxt debug timeout meth step)
       val meths_outcomes = meths_outcomes0
         |> map (apsnd Lazy.value)
         |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
@@ -175,7 +176,7 @@
       preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
         (!preplay_data)
     end
-  | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
+  | set_preplay_outcomes_of_isar_step _ _ _ _ _ _ = ()
 
 fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -34,11 +34,11 @@
     (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
   val string_of_proof_method : proof_method -> string
-  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
+  val tac_of_proof_method : Proof.context -> bool -> thm list * thm list -> proof_method -> int ->
+    tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
   val one_line_proof_text : int -> one_line_params -> string
-  val silence_proof_methods : bool -> Proof.context -> Proof.context
 end;
 
 structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS =
@@ -89,27 +89,36 @@
   | Presburger_Method => "presburger"
   | Algebra_Method => "algebra")
 
-fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
-  Method.insert_tac local_facts THEN'
-  (case meth of
-    Metis_Method (type_enc_opt, lam_trans_opt) =>
-    Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
-      (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
-  | Meson_Method => Meson.meson_tac ctxt global_facts
-  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
-  | _ =>
-    Method.insert_tac global_facts THEN'
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+   exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
+  Try0.silence_methods debug
+  #> Config.put SMT_Config.verbose debug
+
+fun tac_of_proof_method ctxt0 debug (local_facts, global_facts) meth =
+  let val ctxt = silence_proof_methods debug ctxt0 in
+    Method.insert_tac local_facts THEN'
     (case meth of
-      Blast_Method => blast_tac ctxt
-    | Simp_Method => Simplifier.asm_full_simp_tac ctxt
-    | Simp_Size_Method =>
-      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
-    | Auto_Method => K (Clasimp.auto_tac ctxt)
-    | Fastforce_Method => Clasimp.fast_force_tac ctxt
-    | Force_Method => Clasimp.force_tac ctxt
-    | Linarith_Method => Lin_Arith.tac ctxt
-    | Presburger_Method => Cooper.tac true [] [] ctxt
-    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+      Metis_Method (type_enc_opt, lam_trans_opt) =>
+      Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
+        (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
+    | Meson_Method => Meson.meson_tac ctxt global_facts
+
+    | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+    | _ =>
+      Method.insert_tac global_facts THEN'
+      (case meth of
+        Blast_Method => blast_tac ctxt
+      | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+      | Simp_Size_Method =>
+        Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+      | Auto_Method => K (Clasimp.auto_tac ctxt)
+      | Fastforce_Method => Clasimp.fast_force_tac ctxt
+      | Force_Method => Clasimp.force_tac ctxt
+      | Linarith_Method => Lin_Arith.tac ctxt
+      | Presburger_Method => Cooper.tac true [] [] ctxt
+      | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+  end
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
@@ -189,10 +198,4 @@
     try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   end
 
-(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
-   exceeded" warnings and the like. *)
-fun silence_proof_methods debug =
-  Try0.silence_methods debug
-  #> Config.put SMT_Config.verbose debug
-
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -78,7 +78,7 @@
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
-  val play_one_line_proof : mode -> bool -> Time.time -> ((string * 'a) * thm) list ->
+  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
     Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
   val remotify_atp_if_not_installed : theory -> string -> string option
   val isar_supported_prover_of : theory -> string -> string
@@ -219,15 +219,15 @@
     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   end
 
-fun timed_proof_method meth timeout ths =
-  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt ([], ths) meth)
+fun timed_proof_method debug timeout ths meth =
+  timed_apply timeout (fn ctxt => tac_of_proof_method ctxt debug ([], ths) meth)
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
 fun filter_used_facts keep_chained used =
   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
 
-fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred (meths as meth :: _) =
   let
     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   in
@@ -249,7 +249,7 @@
                   ()
               val timer = Timer.startRealTimer ()
             in
-              (case timed_proof_method meth timeout ths state i of
+              (case timed_proof_method debug timeout ths meth state i of
                 SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
               | _ => play timed_out meths)
             end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -353,8 +353,8 @@
           (used_facts,
            Lazy.lazy (fn () =>
              let val used_pairs = used_from |> filter_used_facts false used_facts in
-               play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
-                 meths
+               play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+                 (hd meths) meths
              end),
            fn preplay =>
               let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -50,7 +50,7 @@
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT
 
-fun run_proof_method mode name (params as {verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
     minimize_command
     ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   let
@@ -60,8 +60,8 @@
       else raise Fail ("unknown proof_method: " ^ quote name)
     val used_facts = facts |> map fst
   in
-    (case play_one_line_proof (if mode = Minimize then Normal else mode) verbose timeout facts state
-        subgoal meth [meth] of
+    (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
+        state subgoal meth [meth] of
       play as (_, Played time) =>
       {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
        preplay = Lazy.value play,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Feb 13 13:16:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Feb 13 13:16:17 2014 +0100
@@ -71,7 +71,7 @@
 
 fun weight_smt_fact ctxt num_facts ((info, th), j) =
   let val thy = Proof_Context.theory_of ctxt in
-    (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy))
+    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
   end
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
@@ -212,7 +212,7 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -233,8 +233,8 @@
       (case outcome of
         NONE =>
         (Lazy.lazy (fn () =>
-           play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT_Method
-             (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
          fn preplay =>
             let
               val one_line_params =