diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy
index c9ee26ab1..4fab2d42a 100644
--- a/spec/abstract/Invocations_A.thy
+++ b/spec/abstract/Invocations_A.thy
@@ -41,7 +41,7 @@ datatype tcb_invocation =
     WriteRegisters machine_word bool "machine_word list" arch_copy_register_sets
   | ReadRegisters machine_word bool machine_word arch_copy_register_sets
   | CopyRegisters machine_word machine_word bool bool bool bool arch_copy_register_sets
-  | ThreadControl machine_word cslot_ptr
+  | ThreadControl (tc_target: machine_word) (tc_slot: cslot_ptr)
                   (tc_new_fault_ep: "cap_ref option")
                   (tc_new_mcpriority: "(word8 * obj_ref) option")
                   (tc_new_priority: "(word8 * obj_ref) option")