avoid spurious warnings, notably of 'try0' about already declared simps etc.;
authorwenzelm
Sat, 13 Jul 2013 19:55:53 +0200
changeset 52652 ebdbd5c79a13
parent 52651 5adb5c69af97
child 52653 0589394aaaa5
avoid spurious warnings, notably of 'try0' about already declared simps etc.;
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