diff -r d63f80f93025 -r 51dfdcd88e84 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Thu Jul 18 21:57:27 2013 +0200
+++ b/src/Tools/solve_direct.ML	Thu Jul 18 22:00:35 2013 +0200
@@ -29,6 +29,7 @@
 val noneN = "none";
 val unknownN = "none";
 
+
 (* preferences *)
 
 val max_solutions = Unsynchronized.ref 5;
@@ -46,10 +47,11 @@
 fun do_solve_direct mode state =
   let
     val ctxt = Proof.context_of state;
+    val find_ctxt = if mode = Auto_Try then Context_Position.set_visible false ctxt else ctxt;
 
     val crits = [(true, Find_Theorems.Solves)];
     fun find g =
-      snd (Find_Theorems.find_theorems ctxt (SOME g) (SOME (! max_solutions)) false crits);
+      snd (Find_Theorems.find_theorems find_ctxt (SOME g) (SOME (! max_solutions)) false crits);
 
     fun prt_result (goal, results) =
       let