--- 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