# HG changeset patch
# User wenzelm
# Date 1373738153 -7200
# Node ID ebdbd5c79a1396a935edeadb1456dd6b6e135e75
# Parent  5adb5c69af97a2d94a57ea22e2726da2618d4fde
avoid spurious warnings, notably of 'try0' about already declared simps etc.;

diff -r 5adb5c69af97 -r ebdbd5c79a13 src/Tools/try.ML
--- a/src/Tools/try.ML	Sat Jul 13 18:33:33 2013 +0200
+++ b/src/Tools/try.ML	Sat Jul 13 19:55:53 2013 +0200
@@ -126,6 +126,7 @@
           print_fn = fn _ => fn st =>
             let
               val state = Toplevel.proof_of st
+                |> Proof.map_context (Context_Position.set_visible false)
               val auto_time_limit = Options.default_real @{option auto_time_limit}
             in
               if auto_time_limit > 0.0 then