--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Fri Feb 10 23:30:17 2012 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Fri Feb 10 23:36:02 2012 +0100
@@ -213,7 +213,7 @@
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun writeTextFile name s = File.write (Path.explode name) s
-
+
fun fileExists name = ((OS.FileSys.fileSize name; true) handle OS.SysErr _ => false)
fun compile eqs =
@@ -236,7 +236,7 @@
end
fun readResultFile name = File.read (Path.explode name)
-
+
fun parse_result arity_of result =
let
val result = String.explode result