# HG changeset patch
# User wenzelm
# Date 1431088834 -7200
# Node ID d8a4fe35da00740eef7804bf1489f7976663d463
# Parent  c2837a39da01631064c95c5b69c287d7ad05bc8f
silence local Unify.trace_bound as well: existing tools either refer to Proof.context or theory;

diff -r c2837a39da01 -r d8a4fe35da00 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Fri May 08 10:19:44 2015 +0200
+++ b/src/HOL/Tools/try0.ML	Fri May 08 14:40:34 2015 +0200
@@ -106,12 +106,14 @@
 fun silence_methods debug =
   Config.put Metis_Tactic.verbose debug
   #> Config.put Lin_Arith.verbose debug
-  #> (not debug ?
-    (Context_Position.set_visible false
-     #> 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))));
+  #> not debug ? (fn ctxt =>
+      ctxt
+      |> Context_Position.set_visible false
+      |> Config.put Unify.trace_bound (Config.get ctxt Unify.search_bound)
+      |> 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)));
 
 fun generic_try0 mode timeout_opt quad st =
   let