src/HOL/Matrix/Compute_Oracle/am_ghc.ML
changeset 43850 7f2cbc713344
parent 43602 8c89a1fb30f2
child 46531 eff798e48efc
     1.1 --- a/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ b/src/HOL/Matrix/Compute_Oracle/am_ghc.ML	Sat Jul 16 20:52:41 2011 +0200
     1.3 @@ -227,7 +227,7 @@
     1.4          val module_file = tmp_file (module^".hs")
     1.5          val object_file = tmp_file (module^".o")
     1.6          val _ = writeTextFile module_file source
     1.7 -        val _ = bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
     1.8 +        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ module_file)
     1.9          val _ =
    1.10            if not (fileExists object_file) then
    1.11              raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    1.12 @@ -311,7 +311,7 @@
    1.13          val term = print_term arity_of 0 t
    1.14          val call_source = "module "^call^" where\n\nimport "^module^"\n\ncall = "^module^".calc \""^result_file^"\" ("^term^")"
    1.15          val _ = writeTextFile call_file call_source
    1.16 -        val _ = bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    1.17 +        val _ = Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^module_file^" "^call_file)
    1.18          val result = readResultFile result_file handle IO.Io _ =>
    1.19            raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
    1.20          val t' = parse_result arity_of result