replaced File.sysify_path by Path.pack;
avoid "handle _" (which is not well-defined due to erratic Interrupt exceptions);

--- a/src/HOL/Tools/sat_solver.ML	Sun Jun 05 11:31:33 2005 +0200
+++ b/src/HOL/Tools/sat_solver.ML	Sun Jun 05 11:57:14 2005 +0200
@@ -526,11 +526,11 @@
 		val cmd        = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
-		val _          = (File.rm inpath handle _ => ())
-		val _          = (File.rm outpath handle _ => ())
+		val _          = try File.rm inpath
+		val _          = try File.rm outpath
 	in
 		result
 	end
@@ -551,11 +551,11 @@
 		val cmd        = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("Satisfiable          !!", "solution =", "UNSATISFIABLE          !!")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
-		val _          = (File.rm inpath handle _ => ())
-		val _          = (File.rm outpath handle _ => ())
+		val _          = try File.rm inpath
+		val _          = try File.rm outpath
 	in
 		result
 	end
@@ -576,11 +576,11 @@
 		val cmd        = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath)
 		fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm)
 		fun readfn ()  = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE")
-		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else ()
-		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else ()
+		val _          = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else ()
+		val _          = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else ()
 		val result     = SatSolver.make_external_solver cmd writefn readfn fm
-		val _          = (File.rm inpath handle _ => ())
-		val _          = (File.rm outpath handle _ => ())
+		val _          = try File.rm inpath
+		val _          = try File.rm outpath
 	in
 		result
 	end