suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';

--- a/src/Pure/Tools/find_theorems.ML	Sat Feb 04 19:10:12 2017 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 04 19:48:43 2017 +0100
@@ -183,10 +183,10 @@
 
 fun filter_solves ctxt goal =
   let
-    val thy' =
-      Proof_Context.theory_of ctxt
-      |> Context_Position.set_visible_global (Context_Position.is_visible ctxt);
-    val ctxt' = Proof_Context.transfer thy' ctxt;
+    val thy' = Proof_Context.theory_of ctxt
+      |> Context_Position.set_visible_global false;
+    val ctxt' = Proof_Context.transfer thy' ctxt
+      |> Context_Position.set_visible false;
     val goal' = Thm.transfer thy' goal;
 
     fun limited_etac thm i =

--- a/src/Tools/solve_direct.ML	Sat Feb 04 19:10:12 2017 +0100
+++ b/src/Tools/solve_direct.ML	Sat Feb 04 19:48:43 2017 +0100
@@ -42,12 +42,10 @@
 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;
 
     fun find goal =
-      #2 (Find_Theorems.find_theorems find_ctxt (SOME goal)
-        (SOME (Config.get find_ctxt max_solutions)) false [(true, Find_Theorems.Solves)]);
+      #2 (Find_Theorems.find_theorems ctxt (SOME goal)
+        (SOME (Config.get ctxt max_solutions)) false [(true, Find_Theorems.Solves)]);
 
     fun prt_result (goal, results) =
       let