src/Pure/Concurrent/multithreading.ML
changeset 62826 eb94e570c1a4
parent 62715 8312e5d8d217
child 62891 7a11ea5c9626
     1.1 --- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -127,10 +127,10 @@
     1.4  fun tracing_time detailed time =
     1.5    tracing
     1.6     (if not detailed then 5
     1.7 -    else if Time.>= (time, seconds 1.0) then 1
     1.8 -    else if Time.>= (time, seconds 0.1) then 2
     1.9 -    else if Time.>= (time, seconds 0.01) then 3
    1.10 -    else if Time.>= (time, seconds 0.001) then 4 else 5);
    1.11 +    else if time >= seconds 1.0 then 1
    1.12 +    else if time >= seconds 0.1 then 2
    1.13 +    else if time >= seconds 0.01 then 3
    1.14 +    else if time >= seconds 0.001 then 4 else 5);
    1.15  
    1.16  fun real_time f x =
    1.17    let