src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 41946 380f7f5ff126
parent 41940 a3b68a7a0e15
child 41952 c7297638599b
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 16:14:14 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Mar 13 16:30:02 2011 +0100
@@ -42,9 +42,9 @@
         val _ = File.write code_file code'
         val _ = File.write narrowing_engine_file narrowing_engine
         val _ = File.write main_file main
-        val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
+        val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
         val cmd = "\"$EXEC_GHC\" -fglasgow-exts " ^
-          (space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^
+          (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ " && " ^ executable
       in
         bash_output cmd