proper support for Windows exe;

--- a/src/HOL/Tools/SMT/smt_systems.ML	Thu Oct 15 13:24:16 2020 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Thu Oct 15 13:47:55 2020 +0200
@@ -18,7 +18,9 @@
 fun check_tool var () =
   (case getenv var of
     "" => NONE
-  | s => if File.is_file (Path.variable var) then SOME [s] else NONE);
+  | s =>
+      if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe)
+      then SOME [s] else NONE);
 
 fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
 

--- a/src/Pure/General/path.ML	Thu Oct 15 13:24:16 2020 +0200
+++ b/src/Pure/General/path.ML	Thu Oct 15 13:47:55 2020 +0200
@@ -32,6 +32,7 @@
   val dir: T -> T
   val base: T -> T
   val ext: string -> T -> T
+  val platform_exe: T -> T
   val split_ext: T -> T * string
   val exe: T -> T
   val expand: T -> T
@@ -212,6 +213,8 @@
 fun ext "" = I
   | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
 
+val platform_exe = ML_System.platform_is_windows ? ext "exe";
+
 val split_ext = split_path (fn (prfx, s) => apfst (append prfx)
   (case chop_suffix (fn c => c <> ".") (raw_explode s) of
     ([], _) => (Path [Basic s], "")