--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 13:44:42 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Mar 27 14:33:08 2025 +0100
@@ -292,7 +292,7 @@
fun default_params thy = get_params Normal thy o map (apsnd single)
val silence_state =
- Proof.map_contexts (Try0_Util.silence_methods false #> Config.put SMT_Config.verbose false)
+ Proof.map_contexts (Try0_HOL.silence_methods #> Config.put SMT_Config.verbose false)
(* Sledgehammer the given subgoal *)