src/HOL/Tools/Quickcheck/narrowing_generators.ML

                 (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
           " -o " ^ File.bash_platform_path executable ^ ";"
         val compilation_time =
           Isabelle_System.bash_process cmd
           |> Process_Result.print
-          |> Process_Result.timing |> #elapsed |> Time.toMilliseconds;
+          |> Process_Result.timing_elapsed |> Time.toMilliseconds;
         val _ = Quickcheck.add_timing ("Haskell compilation", compilation_time) current_result
         fun haskell_string_of_bool v = if v then "True" else "False"
         val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
         fun with_size genuine_only k =
           if k > size then (NONE, !current_result)

                 Isabelle_System.bash_process
                   (File.bash_path executable ^ " " ^ haskell_string_of_bool genuine_only ^ " " ^
                     string_of_int k);
               val _ = warning (Process_Result.err res);
               val response = Process_Result.out res;
-              val timing = res |> Process_Result.timing |> #elapsed |> Time.toMilliseconds;
+              val timing = res |> Process_Result.timing_elapsed |> Time.toMilliseconds;
               val _ =
                 Quickcheck.add_timing
                   ("execution of size " ^ string_of_int k, timing) current_result
             in
               if response = "NONE" then with_size genuine_only (k + 1)