--- a/src/HOL/Tools/try0.ML Wed Feb 28 23:50:22 2024 +0100
+++ b/src/HOL/Tools/try0.ML Wed Feb 28 15:19:15 2024 +0100
@@ -109,12 +109,12 @@
ctxt
|> Simplifier_Trace.disable
|> Context_Position.set_visible false
- |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound)
+ |> Config.put Unify.unify_trace_bound (Config.get ctxt Unify.search_bound)
|> Config.put Argo_Tactic.trace "none"
|> Proof_Context.background_theory (fn thy =>
thy
|> Context_Position.set_visible_global false
- |> Config.put_global Unify.trace_bound (Config.get_global thy Unify.search_bound)));
+ |> Config.put_global Unify.unify_trace_bound (Config.get_global thy Unify.search_bound)));
fun generic_try0 mode timeout_opt quad st =
let