slightly more robust bash exec, which fails on empty executable;

--- 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

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 19:16:19 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 19:27:39 2011 +0100
@@ -43,7 +43,7 @@
         val _ = File.write narrowing_engine_file narrowing_engine
         val _ = File.write main_file main
         val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
-        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
+        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ " && " ^ executable
       in