--- a/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Sun Sep 20 20:00:14 2020 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML Sun Sep 20 20:47:59 2020 +0200
@@ -223,8 +223,7 @@
val object_file = tmp_file (module^".o")
val _ = File.write module_file source
val _ =
- Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^
- Bash.string (File.platform_path module_file))
+ Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -c " ^ File.bash_platform_path module_file)
val _ =
if not (File.exists object_file) then
raise Compile ("Failure compiling haskell code (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
@@ -310,8 +309,7 @@
val _ = File.write call_file call_source
val _ =
Isabelle_System.bash ("exec \"$ISABELLE_GHC\" -e \""^call^".call\" "^
- Bash.string (File.platform_path module_file) ^ " " ^
- Bash.string (File.platform_path call_file))
+ File.bash_platform_path module_file ^ " " ^ File.bash_platform_path call_file)
val result = File.read result_file handle IO.Io _ =>
raise Run ("Failure running haskell compiler (ISABELLE_GHC='" ^ getenv "ISABELLE_GHC" ^ "')")
val t' = parse_result arity_of result