# HG changeset patch
# User desharna
# Date 1649487195 -7200
# Node ID 9c2a0b67eb68d5c1f7e2b3b4278b61354330c005
# Parent  b9c6758bb784c78ff61ce6cc9fd998a488c248af
reused slice in Sledgehammer's minimizer

diff -r b9c6758bb784 -r 9c2a0b67eb68 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Apr 07 12:37:42 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Sat Apr 09 08:53:15 2022 +0200
@@ -21,8 +21,8 @@
   val get_slices : Proof.context -> string -> prover_slice list
 
   val binary_min_facts : int Config.T
-  val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
-    Proof.state -> thm -> ((string * stature) * thm list) list ->
+  val minimize_facts : (thm list -> unit) -> string -> params -> prover_slice -> bool -> int ->
+    int -> Proof.state -> thm -> ((string * stature) * thm list) list ->
     ((string * stature) * thm list) list option
     * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
@@ -199,12 +199,11 @@
     | p => p)
   end
 
-fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
-    facts =
+fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) slice silent i n state
+    goal facts =
   let
     val ctxt = Proof.context_of state
     val prover = get_prover ctxt Minimize prover_name
-    val slice = hd (get_slices ctxt prover_name)
     val (chained, non_chained) = List.partition is_fact_chained facts
 
     fun test timeout non_chained =
@@ -239,7 +238,7 @@
   end
 
 fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
-    ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
+    ({state, goal, subgoal, subgoal_count, ...} : prover_problem) slice
     (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
      : prover_result) =
   if is_some outcome then
@@ -248,7 +247,7 @@
     let
       val (used_facts, message) =
         if minimize then
-          minimize_facts do_learn name params
+          minimize_facts do_learn name params slice
             (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
             goal (filter_used_facts true used_facts (map (apsnd single) used_from))
           |>> Option.map (map fst)
@@ -264,6 +263,6 @@
 
 fun get_minimizing_prover ctxt mode do_learn name params problem slice =
   get_prover ctxt mode name params problem slice
-  |> maybe_minimize mode do_learn name params problem
+  |> maybe_minimize mode do_learn name params problem slice
 
 end;