src/Pure/General/timing.ML
changeset 62826 eb94e570c1a4
parent 59149 0070053570c4
child 66416 96ad7d5ff613
     1.1 --- a/src/Pure/General/timing.ML	Sat Apr 02 23:14:08 2016 +0200
     1.2 +++ b/src/Pure/General/timing.ML	Sat Apr 02 23:29:05 2016 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  
     1.5  val min_time = Time.fromMilliseconds 1;
     1.6  
     1.7 -fun is_relevant_time time = Time.>= (time, min_time);
     1.8 +fun is_relevant_time time = time >= min_time;
     1.9  
    1.10  fun is_relevant {elapsed, cpu, gc} =
    1.11    is_relevant_time elapsed orelse