# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1729600285 -7200
# Node ID 6a8dbe8ee252daa33248d0c559e8c58475cd2fe2
# Parent  5ad7c7f825d20fd7b94fc6fd7f1b29bb7b4e42b5
tuned: unused parameter;

diff -r 5ad7c7f825d2 -r 6a8dbe8ee252 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri Nov 08 11:18:08 2024 +0100
+++ b/src/HOL/Tools/try0.ML	Tue Oct 22 14:31:25 2024 +0200
@@ -21,18 +21,18 @@
 
 val default_timeout = seconds 5.0;
 
-fun can_apply timeout_opt pre post tac st =
+fun can_apply timeout_opt post tac st =
   let val {goal, ...} = Proof.goal st in
     (case (case timeout_opt of
             SOME timeout => Timeout.apply_physical timeout
-          | NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
+          | NONE => fn f => fn x => f x) (Seq.pull o tac) st of
       SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
     | NONE => false)
   end;
 
-fun apply_generic timeout_opt name command pre post apply st =
+fun apply_generic timeout_opt name command post apply st =
   let val time_start = Time.now () in
-    if try (can_apply timeout_opt pre post apply) st = SOME true then
+    if try (can_apply timeout_opt post apply) st = SOME true then
       SOME (name, command, Time.toMilliseconds (Time.now () - time_start))
     else
       NONE
@@ -66,7 +66,7 @@
       apply_generic timeout_opt name
         ((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
          (if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
-        I (#goal o Proof.goal)
+        (#goal o Proof.goal)
         (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
           #> Seq.filter_results) st
     end