# HG changeset patch
# User boehmes
# Date 1294403049 -3600
# Node ID a7a03f85635463a933d94bd8bff5071c736ac8df
# Parent  3e0fc4a54ca1128ee927528d4993e12bff23709e
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)

diff -r 3e0fc4a54ca1 -r a7a03f856354 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Fri Jan 07 10:28:45 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML	Fri Jan 07 13:24:09 2011 +0100
@@ -99,15 +99,7 @@
   filter (is_available ctxt) (all_solvers_of ctxt)
 
 fun warn_solver name =
-  let
-    fun app p n = Path.append p (Path.explode n)
-    val path = Path.explode (getenv "ISABELLE_HOME_USER")
-    val path' = app (app path "etc") "components"
-  in
-    warning ("The SMT solver " ^ quote name ^ " is not installed. " ^
-      "Please add the path to its component bundle to " ^
-      "the components list in " ^ quote (Path.implode path') ^ ".")
-  end
+  warning ("The SMT solver " ^ quote name ^ " is not installed.")
 
 fun select_solver name context =
   let