--- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sun Mar 13 19:16:19 2011 +0100
+++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML Sun Mar 13 19:27:39 2011 +0100
@@ -227,7 +227,7 @@
val module_file = tmp_file (module^".hs")
val object_file = tmp_file (module^".o")
val _ = writeTextFile module_file source
- val _ = bash ("\"$ISABELLE_GHC\" -c " ^ module_file)
+ val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
val _ =
if not (fileExists object_file) then
raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -311,7 +311,7 @@
val term = print_term arity_of 0 t
val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
val _ = writeTextFile call_file call_source
- val _ = bash ("\"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
+ val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
val result = readResultFile result_file handle IO.Io _ =>
raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
val t' = parse_result arity_of result