# HG changeset patch
# User haftmann
# Date 1328913362 -3600
# Node ID ddf7cc923d192eb923a9ace8dfefb79b581f4005
# Parent  df192df78614e17aa4eda8c2cc16d1d40aab53da
dropped whitespace

diff -r df192df78614 -r ddf7cc923d19 src/HOL/Matrix/Compute_Oracle/am_ghc.ML
--- 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