src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43850 7f2cbc713344
parent 43702 24fb44c1086a
child 43878 eeb10fdd9535
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:14:58 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sat Jul 16 20:52:41 2011 +0200
     1.3 @@ -253,9 +253,10 @@
     1.4          val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
     1.5            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
     1.6            " -o " ^ executable ^ ";"
     1.7 -        val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd) 
     1.8 +        val (result, compilation_time) =
     1.9 +          elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) 
    1.10          val _ = Quickcheck.add_timing compilation_time current_result
    1.11 -        val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.12 +        val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.13          fun with_size k =
    1.14            if k > size then
    1.15              (NONE, !current_result)
    1.16 @@ -264,7 +265,7 @@
    1.17                val _ = message ("Test data size: " ^ string_of_int k)
    1.18                val _ = current_size := k
    1.19                val ((response, _), timing) = elapsed_time ("execution of size " ^ string_of_int k)
    1.20 -                (fn () => bash_output (executable ^ " " ^ string_of_int k))
    1.21 +                (fn () => Isabelle_System.bash_output (executable ^ " " ^ string_of_int k))
    1.22                val _ = Quickcheck.add_timing timing current_result
    1.23              in
    1.24                if response = "NONE\n" then