diff --git a/model/basic/schedule.v b/model/basic/schedule.v
index ec938aab7da97b2e05f6df984b5e7ab427c07262..59a423fb2082874db98d926cb8bc643d814d253f 100644
--- a/model/basic/schedule.v
+++ b/model/basic/schedule.v
@@ -51,7 +51,7 @@ Module Schedule.
       [exists cpu, scheduled_on cpu t].
 
     (* A processor cpu is idle at time t if it doesn't contain any jobs. *)
-    Definition is_idle (cpu: 'I_(num_cpus)) (t: time) :=
+    Definition is_idle (cpu: processor num_cpus) (t: time) :=
       sched cpu t = None.
 
     (* The instantaneous service of job j at time t is the number of cpus