diff -r cc85ccb1a6b2 -r d2960b321468 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Mar 27 10:30:28 2025 +0100
+++ b/src/HOL/Tools/try0.ML	Thu Mar 27 11:20:59 2025 +0100
@@ -6,7 +6,6 @@
 
 signature TRY0 =
 sig
-  val silence_methods : bool -> Proof.context -> Proof.context
   datatype modifier = Use | Simp | Intro | Elim | Dest
   type xref = Facts.ref * Token.src list
   type tagged_xref = xref * modifier list
@@ -17,9 +16,9 @@
   val register_proof_method : string -> proof_method_options -> proof_method -> unit
   val get_proof_method : string -> proof_method option
 
-  val apply_proof_method : string -> Time.time option -> tagged_xref list ->
-    Proof.state -> result option
   val try0 : Time.time option -> tagged_xref list -> Proof.state -> result list
+
+  val silence_methods : bool -> Proof.context -> Proof.context
 end
 
 structure Try0 : TRY0 =
@@ -31,47 +30,10 @@
 
 val default_timeout = seconds 5.0
 
-fun run_tac timeout_opt tac st =
-  let val with_timeout =
-    (case timeout_opt of SOME timeout => Timeout.apply_physical timeout | NONE => I)
-  in with_timeout (Seq.pull o tac) st |> Option.map fst end
-
-val num_goals = Thm.nprems_of o #goal o Proof.goal
-fun apply_recursive recurse elapsed0 timeout_opt apply st =
-  (case Timing.timing (Option.join o try (run_tac timeout_opt apply)) st of
-    ({elapsed, ...}, SOME st') =>
-      if recurse andalso num_goals st' > 0 andalso num_goals st' < num_goals st then
-        let val timeout_opt1 = (Option.map (fn timeout => timeout - elapsed) timeout_opt)
-        in apply_recursive recurse (elapsed0 + elapsed) timeout_opt1 apply st' end
-      else (elapsed0 + elapsed, st')
-   |_ => (elapsed0, st))
-
-fun parse_method ctxt s =
-  enclose "(" ")" s
-  |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
-  |> filter Token.is_proper
-  |> Scan.read Token.stopper Method.parse
-  |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source")
-
 datatype modifier = Use | Simp | Intro | Elim | Dest
 type xref = Facts.ref * Token.src list
 type tagged_xref = xref * modifier list
 
-fun string_of_xref ((xref, args) : xref) =
-  (case xref of
-    Facts.Fact literal => literal |> Symbol_Pos.explode0 |> Symbol_Pos.implode |> cartouche
-  | _ =>
-      Facts.string_of_ref xref) ^ implode
-        (map (enclose "[" "]" o Pretty.unformatted_string_of o Token.pretty_src \<^context>) args)
-
-fun add_attr_text (tagged : tagged_xref list) (tag, src) s =
-  let
-    val fs = tagged |> filter (fn (_, tags) => member (op =) tags tag) |> map (string_of_xref o fst)
-  in if null fs then s else s ^ " " ^ (if src = "" then "" else src ^ ": ") ^ implode_space fs end
-
-fun attrs_text tags (tagged : tagged_xref list) =
-  "" |> fold (add_attr_text tagged) tags
-
 type result = {name: string, command: string, time: Time.time, state: Proof.state}
 type proof_method = Time.time option -> tagged_xref list -> Proof.state -> result option
 type proof_method_options = {run_if_auto_try: bool}
@@ -129,20 +91,8 @@
 fun time_string time = string_of_int (Time.toMilliseconds time) ^ " ms"
 fun tool_time_string (s, time) = s ^ ": " ^ time_string time
 
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
-   bound exceeded" warnings and the like. *)
-fun silence_methods debug =
-  Config.put Metis_Tactic.verbose debug
-  #> not debug ? (fn ctxt =>
-      ctxt
-      |> Simplifier_Trace.disable
-      |> Context_Position.set_visible false
-      |> Config.put Unify.unify_trace false
-      |> Config.put Argo_Tactic.trace "none")
-
 fun generic_try0 mode timeout_opt (tagged : tagged_xref list) st =
   let
-    val st = Proof.map_contexts (silence_methods false) st
     fun try_method method = method mode timeout_opt tagged st
     fun get_message {command, time, ...} = "Found proof: " ^ Active.sendback_markup_command
       command ^ " (" ^ time_string time ^ ")"
@@ -216,81 +166,15 @@
    {name = "try0", weight = 30, auto_option = \<^system_option>\<open>auto_methods\<close>,
     body = fn auto => fst o generic_try0 (if auto then Auto_Try else Try) NONE []}
 
-
-local
-
-val full_attrs = [(Simp, "simp"), (Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
-val clas_attrs = [(Intro, "intro"), (Elim, "elim"), (Dest, "dest")]
-val simp_attrs = [(Simp, "add")]
-val metis_attrs = [(Simp, ""), (Intro, ""), (Elim, ""), (Dest, "")]
-val no_attrs = []
-
-(* name * (run_if_auto_try * (all_goals * tags)) *)
-val raw_named_methods =
-  [("simp", (true, (false, simp_attrs))),
-   ("auto", (true, (true, full_attrs))),
-   ("blast", (true, (false, clas_attrs))),
-   ("metis", (true, (false, metis_attrs))),
-   ("argo", (true, (false, no_attrs))),
-   ("linarith", (true, (false, no_attrs))),
-   ("presburger", (true, (false, no_attrs))),
-   ("algebra", (true, (false, no_attrs))),
-   ("fast", (false, (false, clas_attrs))),
-   ("fastforce", (false, (false, full_attrs))),
-   ("force", (false, (false, full_attrs))),
-   ("meson", (false, (false, metis_attrs))),
-   ("satx", (false, (false, no_attrs))),
-   ("order", (true, (false, no_attrs)))]
-
-fun apply_raw_named_method name (all_goals, attrs) timeout_opt tagged st :
-    result option =
-  let
-    val unused =
-      tagged
-      |> filter
-        (fn (_, tags) => not (null tags) andalso null (inter (op =) tags (attrs |> map fst)))
-      |> map fst
-
-    val attrs = attrs_text attrs tagged
-
-    val ctxt = Proof.context_of st
-
-    val text =
-      name ^ attrs
-      |> parse_method ctxt
-      |> Method.method_cmd ctxt
-      |> Method.Basic
-      |> (fn m => Method.Combinator (Method.no_combinator_info, Method.Select_Goals 1, [m]))
-
-    val apply =
-      Proof.using [Attrib.eval_thms ctxt unused |> map (rpair [] o single)]
-      #> Proof.refine text #> Seq.filter_results
-    val num_before = num_goals st
-    val multiple_goals = all_goals andalso num_before > 1
-    val (time, st') = apply_recursive multiple_goals Time.zeroTime timeout_opt apply st
-    val num_after = num_goals st'
-    val select = "[" ^ string_of_int (num_before - num_after)  ^ "]"
-    val unused = implode_space (unused |> map string_of_xref)
-    val command =
-      (if unused <> "" then "using " ^ unused ^ " " else "") ^
-      (if num_after = 0 then "by " else "apply ") ^
-      (name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
-      (if multiple_goals andalso num_after > 0 then select else "")
-  in
-    if num_before > num_after then
-      SOME {name = name, command = command, time = time, state = st'}
-    else NONE
-  end
-
-in
-
-val () = raw_named_methods
-  |> List.app (fn (name, (run_if_auto_try, raw_method)) =>
-    let val meth : proof_method = apply_raw_named_method name raw_method in
-      register_proof_method name {run_if_auto_try = run_if_auto_try} meth
-      handle Symtab.DUP _ => ()
-    end)
+(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
+   bound exceeded" warnings and the like. *)
+fun silence_methods debug =
+  Config.put Metis_Tactic.verbose debug
+  #> not debug ? (fn ctxt =>
+      ctxt
+      |> Simplifier_Trace.disable
+      |> Context_Position.set_visible false
+      |> Config.put Unify.unify_trace false
+      |> Config.put Argo_Tactic.trace "none")
 
 end
-
-end