# HG changeset patch
# User wenzelm
# Date 1460646235 -7200
# Node ID 61b32a6d87e9462dbfb50ff7e6372ad3266f8a1d
# Parent  ba9072b303a21fb1ec3ce2159f7e9df8cf1ab121
more silence;

diff -r ba9072b303a2 -r 61b32a6d87e9 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Thu Apr 14 16:59:47 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Apr 14 17:03:55 2016 +0200
@@ -108,6 +108,7 @@
   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)
       |> Proof_Context.background_theory (fn thy =>