shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
authorboehmes
Fri, 07 Jan 2011 13:24:09 +0100
changeset 41441 a7a03f856354
parent 41440 3e0fc4a54ca1
child 41442 4cfb51a5a444
child 41458 5eca258324ca
child 41460 ea56b98aee83
shortened the warning about uninstalled SMT solvers (the additional hint might get obsolete without further notice)
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