# HG changeset patch
# User blanchet
# Date 1677654051 -3600
# Node ID f6cb40234009d76008284a7f67a4ee750c481b29
# Parent  a15f0fcff04143419cbc9010bb98e43439eda8cf
tuning

diff -r a15f0fcff041 -r f6cb40234009 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -95,7 +95,7 @@
     |> the_default (SH_Unknown, "")
   end
 
-fun play_one_line_proofs minimize timeout used_facts state i methss =
+fun play_one_line_proofs minimize timeout used_facts state goal i methss =
   (if timeout = Time.zeroTime then
      []
    else
@@ -103,7 +103,7 @@
        val ctxt = Proof.context_of state
        val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts
        val fact_names = map fst used_facts
-       val {facts = chained, goal, ...} = Proof.goal state
+       val {facts = chained, ...} = Proof.goal state
        val goal_t = Logic.get_goal (Thm.prop_of goal) i
 
        fun try_methss ress [] = ress
@@ -225,7 +225,7 @@
    |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
  end
 
-fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state subgoal
+fun preplay_prover_result ({minimize, preplay_timeout, ...} : params) state goal subgoal
     (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) =
   let
     val (output, chosen_preplay_outcome) =
@@ -238,7 +238,7 @@
       else
         let
           val preplay_results =
-            play_one_line_proofs minimize preplay_timeout used_facts state subgoal
+            play_one_line_proofs minimize preplay_timeout used_facts state goal subgoal
               (snd preferred_methss)
           val chosen_preplay_outcome =
             select_one_line_proof used_facts (fst preferred_methss) preplay_results
@@ -320,12 +320,12 @@
          found_something = found_something "an inconsistency"}
       end
 
-    val problem = problem |> check_consistent ? flip_problem
+    val problem as {goal, ...} = problem |> check_consistent ? flip_problem
 
     fun really_go () =
       launch_prover params mode learn problem slice prover_name
       |> (if check_consistent then analyze_prover_result_for_consistency else
-        preplay_prover_result params state subgoal)
+        preplay_prover_result params state goal subgoal)
 
     fun go () =
       if debug then