only print warning in a visible context (previously, the warning was printed more than once)

--- a/src/HOL/Tools/SMT/smt_config.ML	Mon Jan 10 17:39:54 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Jan 10 17:41:45 2011 +0100
@@ -98,8 +98,9 @@
 fun available_solvers_of ctxt =
   filter (is_available ctxt) (all_solvers_of ctxt)
 
-fun warn_solver name =
-  warning ("The SMT solver " ^ quote name ^ " is not installed.")
+fun warn_solver context name =
+  Context_Position.if_visible_proof context
+    warning ("The SMT solver " ^ quote name ^ " is not installed.")
 
 fun select_solver name context =
   let
@@ -108,7 +109,8 @@
   in
     if not (member (op =) (all_solvers_of ctxt) name) then
       error ("Trying to select unknown solver: " ^ quote name)
-    else if not (is_available ctxt name) then (warn_solver name; upd context)
+    else if not (is_available ctxt name) then
+      (warn_solver context name; upd context)
     else upd context
   end