# HG changeset patch
# User blanchet
# Date 1391467113 -3600
# Node ID dc68f6fb88d291e00136d6a6c0391cf31ac60904
# Parent  59ab33f9d4de056dd80d8b67a9bf72889eb2bcd4
properly overwrite replay data from one compression iteration to another

diff -r 59ab33f9d4de -r dc68f6fb88d2 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 23:38:33 2014 +0100
@@ -172,8 +172,8 @@
         |> map (apsnd Lazy.value)
         |> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
     in
-      preplay_data := Canonical_Label_Tab.map_default (l, [])
-        (fold (AList.update (op =)) meths_outcomes) (!preplay_data)
+      preplay_data := Canonical_Label_Tab.update (l, fold (AList.update (op =)) meths_outcomes [])
+        (!preplay_data)
     end
   | set_preplay_outcomes_of_isar_step _ _ _ _ _ = ()
 
diff -r 59ab33f9d4de -r dc68f6fb88d2 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 23:38:33 2014 +0100
@@ -77,7 +77,7 @@
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
-  val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
+  val play_one_line_proof : mode -> 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
@@ -223,7 +223,7 @@
 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 debug verbose timeout pairs state i preferred (meths as meth :: _) =
+fun play_one_line_proof mode verbose timeout pairs state i preferred (meths as meth :: _) =
   let
     fun get_preferred meths = if member (op =) meths preferred then preferred else meth
   in
diff -r 59ab33f9d4de -r dc68f6fb88d2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 23:38:33 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 debug verbose preplay_timeout used_pairs state subgoal
-                 (hd meths) meths
+               play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
+                 meths
              end),
            fn preplay =>
               let
diff -r 59ab33f9d4de -r dc68f6fb88d2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 23:38:33 2014 +0100
@@ -50,7 +50,7 @@
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT
 
-fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {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) debug verbose timeout facts
-       state subgoal meth [meth] of
+    (case play_one_line_proof (if mode = Minimize then Normal else mode) 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,
diff -r 59ab33f9d4de -r dc68f6fb88d2 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 23:38:33 2014 +0100
@@ -212,7 +212,7 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {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 debug verbose preplay_timeout used_pairs state subgoal
-             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+           play_one_line_proof mode 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 =