src/HOL/Tools/try0.ML

   Config.put Metis_Tactic.verbose debug
   #> not debug ? (fn ctxt =>
       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
     val st = Proof.map_contexts (silence_methods false) st;
     fun trd (_, _, t) = t;