# HG changeset patch
# User desharna
# Date 1743440145 -7200
# Node ID 44440263d847e479fb03fe2a710bb9f321d56db7
# Parent  0f8a51fedae6bc1d2fce0a7ef34203c76c7cba90
tuned signature

diff -r 0f8a51fedae6 -r 44440263d847 src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Mar 31 16:53:14 2025 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_tactic.ML	Mon Mar 31 18:55:45 2025 +0200
@@ -11,21 +11,6 @@
   type prover = Sledgehammer_Prover.prover
   type base_slice = Sledgehammer_ATP_Systems.base_slice
 
-  val algebraN : string
-  val argoN : string
-  val autoN : string
-  val blastN : string
-  val fastforceN : string
-  val forceN : string
-  val linarithN : string
-  val mesonN : string
-  val metisN : string
-  val orderN : string
-  val presburgerN : string
-  val satxN : string
-  val simpN : string
-
-  val tactic_provers : string list
   val is_tactic_prover : string -> bool
   val good_slices_of_tactic_prover : string -> base_slice list
   val run_tactic_prover : mode -> string -> prover
@@ -40,25 +25,7 @@
 open Sledgehammer_Proof_Methods
 open Sledgehammer_Prover
 
-val algebraN = "algebra"
-val argoN = "argo"
-val autoN = "auto"
-val blastN = "blast"
-val fastforceN = "fastforce"
-val forceN = "force"
-val linarithN = "linarith"
-val mesonN = "meson"
-val metisN = "metis"
-val orderN = "order"
-val presburgerN = "presburger"
-val satxN = "satx"
-val simpN = "simp"
-
-val tactic_provers =
-  [algebraN, argoN, autoN, blastN, fastforceN, forceN, linarithN, mesonN,
-   metisN, orderN, presburgerN, satxN, simpN]
-
-val is_tactic_prover = member (op =) tactic_provers
+val is_tactic_prover : string -> bool = is_some o Try0.get_proof_method
 
 val meshN = "mesh"
 
@@ -69,21 +36,20 @@
    (1, false, false, 8, meshN),
    (1, false, false, 32, meshN)]
 
-fun meth_of name =
-  if name = algebraN then Algebra_Method
-  else if name = argoN then Argo_Method
-  else if name = autoN then Auto_Method
-  else if name = blastN then Blast_Method
-  else if name = fastforceN then Fastforce_Method
-  else if name = forceN then Force_Method
-  else if name = linarithN then Linarith_Method
-  else if name = mesonN then Meson_Method
-  else if name = metisN then Metis_Method (NONE, NONE, [])
-  else if name = orderN then Order_Method
-  else if name = presburgerN then Presburger_Method
-  else if name = satxN then SATx_Method
-  else if name = simpN then Simp_Method
-  else error ("Unknown tactic: " ^ quote name)
+fun meth_of "algebra" = Algebra_Method
+  | meth_of "argo" = Argo_Method
+  | meth_of "auto" = Auto_Method
+  | meth_of "blast" = Blast_Method
+  | meth_of "fastforce" = Fastforce_Method
+  | meth_of "force" = Force_Method
+  | meth_of "linarith" = Linarith_Method
+  | meth_of "meson" = Meson_Method
+  | meth_of "metis" = Metis_Method (NONE, NONE, [])
+  | meth_of "order" = Order_Method
+  | meth_of "presburger" = Presburger_Method
+  | meth_of "satx" = SATx_Method
+  | meth_of "simp" = Simp_Method
+  | meth_of _ = Metis_Method (NONE, NONE, [])
 
 fun run_tactic_prover mode name ({slices, timeout, ...} : params)
     ({state, goal, subgoal, subgoal_count, factss, found_something, ...} : prover_problem) slice =