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