diff -r 9bc33476f6ac -r 85911b8a6868 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -101,8 +101,9 @@
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver (Context.Proof ctxt) name =
-      Context_Position.if_visible ctxt
+      if Context_Position.is_visible ctxt then
         warning ("The SMT solver " ^ quote name ^ " is not installed.")
+      else ()
   | warn_solver _ _ = ();
 
 fun select_solver name context =