diff -r 9b34b1449cb7 -r f698f76a3713 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Sat Jun 27 10:26:42 2009 +0200
+++ b/src/Pure/General/file.ML	Sat Jun 27 17:34:48 2009 +0200
@@ -12,7 +12,7 @@
   val pwd: unit -> Path.T
   val full_path: Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
-  val isabelle_tool: string -> int
+  val isabelle_tool: string -> string -> int
   val system_command: string -> unit
   eqtype ident
   val rep_ident: ident -> string
@@ -65,7 +65,17 @@
 
 (* system commands *)
 
-fun isabelle_tool cmd = system ("\"$ISABELLE_TOOL\" " ^ cmd);
+fun isabelle_tool name args =
+  (case space_explode ":" (getenv "ISABELLE_TOOLS") |> get_first (fn dir =>
+      let val path = dir ^ "/" ^ name in
+        if can OS.FileSys.modTime path andalso
+          not (OS.FileSys.isDir path) andalso
+          OS.FileSys.access (path, [OS.FileSys.A_READ, OS.FileSys.A_EXEC])
+        then SOME path
+        else NONE
+      end handle OS.SysErr _ => NONE) of
+    SOME path => system (shell_quote path ^ " " ^ args)
+  | NONE => (writeln ("Unknown Isabelle tool: " ^ name); 2));
 
 fun system_command cmd =
   if system cmd <> 0 then error ("System command failed: " ^ cmd)