# HG changeset patch
# User desharna
# Date 1740501833 -3600
# Node ID 7e45a83373c89af4cd33bca10bad60b45fd5df41
# Parent  80ced0c233d94523911118f2e81c04ca61b715a5
tuned time slicing (from Jasmin)

diff -r 80ced0c233d9 -r 7e45a83373c8 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:43:48 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Tue Feb 25 17:43:53 2025 +0100
@@ -40,13 +40,12 @@
 
 val meshN = "mesh"
 
-fun good_slices_of_tactic_prover name =
+fun good_slices_of_tactic_prover _ =
   (* FUDGE *)
   [(1, false, false, 0, meshN),
    (1, false, false, 2, meshN),
-   (1, false, false, 4, meshN),
    (1, false, false, 8, meshN),
-   (1, false, false, 16, meshN)]
+   (1, false, false, 32, meshN)]
 
 (* In sync with Sledgehammer_Proof_Methods.tac_of_proof_method *)
 fun tac_of ctxt name (local_facts, global_facts) =
@@ -82,8 +81,10 @@
 
     val (local_facts, global_facts) =
       ([], [])
-      |> fold (fn fact => if fst (snd (fst fact)) = Global then apsnd (cons (snd fact))
-        else apfst (cons (snd fact))) facts
+      |> fold (fn ((_, (scope, _)), thm) =>
+        if scope = Global then apsnd (cons thm)
+        else if scope = Chained then I
+        else apfst (cons thm)) facts
       |> apfst (append chained)
 
     val timer = Timer.startRealTimer ()