# HG changeset patch
# User wenzelm
# Date 1614014378 -3600
# Node ID a97ae083cad120b683f350691895857412936466
# Parent  057d8a164a7bdf7da968faf8dc9d6ede1621f3aa
tuned signature;

diff -r 057d8a164a7b -r a97ae083cad1 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 18:16:56 2021 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Feb 22 18:19:38 2021 +0100
@@ -264,7 +264,7 @@
         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 ()
@@ -280,7 +280,7 @@
                     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
diff -r 057d8a164a7b -r a97ae083cad1 src/Pure/System/process_result.ML
--- a/src/Pure/System/process_result.ML	Mon Feb 22 18:16:56 2021 +0100
+++ b/src/Pure/System/process_result.ML	Mon Feb 22 18:19:38 2021 +0100
@@ -16,6 +16,7 @@
   val out_lines: T -> string list
   val err_lines: T -> string list
   val timing: T -> Timing.timing
+  val timing_elapsed: T -> Time.time
   val out: T -> string
   val err: T -> string
   val ok: T -> bool
@@ -40,7 +41,9 @@
 val rc = #rc o rep;
 val out_lines = #out_lines o rep;
 val err_lines = #err_lines o rep;
+
 val timing = #timing o rep;
+val timing_elapsed = #elapsed o timing;
 
 end;