# HG changeset patch
# User wenzelm
# Date 1486234123 -3600
# Node ID 481b2855ee9adc5488421520f73c8b6f77e851db
# Parent  c515464b46524e1fad443452b3a6e290012fed18
suppress warnings uniformly, even in explicit commands 'find_theorems', 'solve_direct';

diff -r c515464b4652 -r 481b2855ee9a src/Pure/Tools/find_theorems.ML
--- 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 =
diff -r c515464b4652 -r 481b2855ee9a src/Tools/solve_direct.ML
--- 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