src/HOL/Matrix_LP/Compute_Oracle/am_ghc.ML
changeset 72278 199dc903131b
parent 65905 6181ccb4ec8c
--- 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