src/HOL/Tools/SMT2/smt2_config.ML

--- a/src/HOL/Tools/SMT2/smt2_config.ML	Wed Mar 26 14:15:34 2014 +0100
+++ b/src/HOL/Tools/SMT2/smt2_config.ML	Wed Mar 26 14:41:52 2014 +0100
@@ -99,8 +99,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 =